axiom andER: !P:prop.!Q:prop.P & Q -> Q claim !P:prop.!Q:prop.(P <-> Q) -> Q -> P