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