Theorem 3jaod 1456

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 1452	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))

Syntax hints:   → wi 4   ∨ w3o 1102

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 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105

This theorem is referenced by:  3jaodan  1458  3jaaoOLD  1461  fntpb  7207  dfwe2  7769  poseq  8150  smo11  8347  smoord  8348  omeulem1  8563  omopth2  8565  oaabs2  8631  elfiun  9386  r111  9743  r1pwss  9752  pwcfsdom  10563  winalim2  10676  xmullem  13285  xmulasslem  13306  xlemul1a  13309  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  fvf1tp  13818  symgvalstruct  19462  ordtbas2  23348  ordtbas  23349  fmfnfmlem4  24114  dyadmbl  25759  scvxcvx  27150  perfectlem2  27394  2sq2  27597  ostth3  27802  ltssolem1  27839  addsproplem7  28168  negsproplem7  28227  mulsproplem5  28313  mulsproplem6  28314  mulsproplem7  28315  mulsproplem8  28316  satfun  35903  lineext  36568  fscgr  36572  colinbtwnle  36610  broutsideof2  36614  lineunray  36639  lineelsb2  36640  elicc3  36828  4atlem11  40383  dalawlem10  40654  3cubeslem1  43415  dflim5  44056  omabs2  44059  omcl3g  44061  naddwordnexlem4  44128  frege129d  44489  goldbachth  48299  perfectALTVlem2  48487  gpgiedgdmellem  48811  gpgusgralem  48821  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgedgiov  48830  gpgedg2ov  48831  gpgedg2iv  48832  gpgnbgrvtx0  48839  gpgnbgrvtx1  48840  pgnioedg1  48873  pgnioedg2  48874  pgnioedg3  48875  pgnioedg4  48876  pgnioedg5  48877  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem2  48882  pgnbgreunbgrlem4  48884  pgnbgreunbgrlem5lem1  48885  pgnbgreunbgrlem5lem2  48886  pgnbgreunbgrlem5lem3  48887  pgnbgreunbgrlem5  48888  eenglngeehlnmlem1  49517  eenglngeehlnmlem2  49518