Metamath Proof Explorer


Theorem jc

Description: Deduction joining the consequents of two premises. A deduction associated with pm3.2im . (Contributed by NM, 28-Dec-1992)

Ref Expression
Hypotheses jc.1 φψ
jc.2 φχ
Assertion jc φ¬ψ¬χ

Proof

Step Hyp Ref Expression
1 jc.1 φψ
2 jc.2 φχ
3 pm3.2im ψχ¬ψ¬χ
4 1 2 3 sylc φ¬ψ¬χ