Theorem 3jaod 1428

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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaodan  1430  3jaao  1432  fntpb  7228  dfwe2  7792  poseq  8181  smo11  8402  smoord  8403  omeulem1  8618  omopth2  8620  oaabs2  8685  elfiun  9467  r111  9812  r1pwss  9821  pwcfsdom  10620  winalim2  10733  xmullem  13302  xmulasslem  13323  xlemul1a  13326  xrsupsslem  13345  xrinfmsslem  13346  xrub  13350  fvf1tp  13825  symgvalstruct  19428  symgvalstructOLD  19429  ordtbas2  23214  ordtbas  23215  fmfnfmlem4  23980  dyadmbl  25648  scvxcvx  27043  perfectlem2  27288  2sq2  27491  ostth3  27696  sltsolem1  27734  addsproplem7  28022  negsproplem7  28080  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  satfun  35395  lineext  36057  fscgr  36061  colinbtwnle  36099  broutsideof2  36103  lineunray  36128  lineelsb2  36129  elicc3  36299  4atlem11  39591  dalawlem10  39862  3cubeslem1  42671  dflim5  43318  omabs2  43321  omcl3g  43323  naddwordnexlem4  43390  frege129d  43752  goldbachth  47471  perfectALTVlem2  47646  gpgedgel  47942  gpgusgralem  47945  gpgvtxedg0  47955  gpgvtxedg1  47956  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587