Metamath Proof Explorer


Theorem jcn

Description: Theorem joining the consequents of two premises. Theorem 8 of Margaris p. 60. (Contributed by NM, 5-Aug-1993) (Proof shortened by Josh Purinton, 29-Dec-2000)

Ref Expression
Assertion jcn φ ¬ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 pm2.27 φ φ ψ ψ
2 1 con3d φ ¬ ψ ¬ φ ψ