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