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