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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ∨ 𝜏 ) → 𝜒 ) )