Metamath Proof Explorer

Theorem con4i

Description: Inference associated with con4 . Its associated inference is mt4 .

Remark: this can also be proved using notnot followed by nsyl2 , giving a shorter proof but depending on more axioms (namely, ax-1 and ax-2 ). (Contributed by NM, 29-Dec-1992)

Ref Expression
Hypothesis con4i.1 ¬ φ ¬ ψ
Assertion con4i ψ φ


Step Hyp Ref Expression
1 con4i.1 ¬ φ ¬ ψ
2 con4 ¬ φ ¬ ψ ψ φ
3 1 2 ax-mp ψ φ