Theorem jad

Description: Deduction form of ja . (Contributed by Scott Fenton, 13-Dec-2010) (Proof shortened by Andrew Salmon, 17-Sep-2011)

	Ref	Expression
Hypotheses	jad.1	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜃 ) )
	jad.2	⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
Assertion	jad	⊢ ( 𝜑 → ( ( 𝜓 → 𝜒 ) → 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		jad.1	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜃 ) )
2		jad.2	⊢ ( 𝜑 → ( 𝜒 → 𝜃 ) )
3	1	com12	⊢ ( ¬ 𝜓 → ( 𝜑 → 𝜃 ) )
4	2	com12	⊢ ( 𝜒 → ( 𝜑 → 𝜃 ) )
5	3 4	ja	⊢ ( ( 𝜓 → 𝜒 ) → ( 𝜑 → 𝜃 ) )
6	5	com12	⊢ ( 𝜑 → ( ( 𝜓 → 𝜒 ) → 𝜃 ) )