Metamath Proof Explorer


Theorem annim

Description: Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion annim φ¬ψ¬φψ

Proof

Step Hyp Ref Expression
1 iman φψ¬φ¬ψ
2 1 con2bii φ¬ψ¬φψ