Theorem 3jaod

Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005)

	Ref	Expression
Hypotheses	3jaod.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	3jaod.2	⊢ ( 𝜑 → ( 𝜃 → 𝜒 ) )
	3jaod.3	⊢ ( 𝜑 → ( 𝜏 → 𝜒 ) )
Assertion	3jaod	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		3jaod.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		3jaod.2	⊢ ( 𝜑 → ( 𝜃 → 𝜒 ) )
3		3jaod.3	⊢ ( 𝜑 → ( 𝜏 → 𝜒 ) )
4		3jao	⊢ ( ( ( 𝜓 → 𝜒 ) ∧ ( 𝜃 → 𝜒 ) ∧ ( 𝜏 → 𝜒 ) ) → ( ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) → 𝜒 ) )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) → 𝜒 ) )