This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ¬ ( 𝜓 → ¬ 𝜒 ) )