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