Metamath Proof Explorer


Theorem iman

Description: Implication in terms of conjunction and negation. Theorem 3.4(27) of Stoll p. 176. (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 30-Oct-2012)

Ref Expression
Assertion iman φ ψ ¬ φ ¬ ψ

Proof

Step Hyp Ref Expression
1 notnotb ψ ¬ ¬ ψ
2 1 imbi2i φ ψ φ ¬ ¬ ψ
3 imnan φ ¬ ¬ ψ ¬ φ ¬ ψ
4 2 3 bitri φ ψ ¬ φ ¬ ψ