Theorem 3jaod 1427

Description: Disjunction of three 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 1424	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1370	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))

Syntax hints:   → wi 4   ∨ w3o 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaodan  1429  3jaao  1432  fntpb  7213  dfwe2  7765  poseq  8149  smo11  8370  smoord  8371  omeulem1  8588  omopth2  8590  oaabs2  8654  elfiun  9431  r111  9776  r1pwss  9785  pwcfsdom  10584  winalim2  10697  xmullem  13250  xmulasslem  13271  xlemul1a  13274  xrsupsslem  13293  xrinfmsslem  13294  xrub  13298  symgvalstruct  19312  symgvalstructOLD  19313  ordtbas2  23015  ordtbas  23016  fmfnfmlem4  23781  dyadmbl  25449  scvxcvx  26831  perfectlem2  27076  2sq2  27279  ostth3  27484  sltsolem1  27521  addsproplem7  27805  negsproplem7  27859  mulsproplem5  27933  mulsproplem6  27934  mulsproplem7  27935  mulsproplem8  27936  satfun  34866  lineext  35518  fscgr  35522  colinbtwnle  35560  broutsideof2  35564  lineunray  35589  lineelsb2  35590  elicc3  35666  4atlem11  38944  dalawlem10  39215  3cubeslem1  41885  dflim5  42542  omabs2  42545  omcl3g  42547  naddwordnexlem4  42615  frege129d  42977  goldbachth  46674  perfectALTVlem2  46849  eenglngeehlnmlem1  47585  eenglngeehlnmlem2  47586