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