Theorem 3jaod 1338

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

Hypotheses

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

Assertion

Ref	Expression
3jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))

Proof of Theorem 3jaod

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

Syntax hints:   → wi 4   ∨ w3o 1001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004

This theorem is referenced by:  3jaodan  1340  3jaao  1342  issod  4414  nnawordex  6692  exmidontri2or  7451  addlocprlem  7745  nqprloc  7755  ltexprlemrl  7820  aptiprleml  7849  aptiprlemu  7850  elnn0z  9482  zaddcl  9509  zletric  9513  zlelttric  9514  zltnle  9515  zdceq  9545  zdcle  9546  zdclt  9547  nn01to3  9841  xposdif  10107  fzdcel  10265  qletric  10491  qlelttric  10492  qltnle  10493  qdceq  10494  qdclt  10495  frec2uzlt2d  10656  perfectlem2  15714  triap  16569  tridceq  16596