Theorem 3jaod 1454

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

Syntax hints:   → wi 4   ∨ w3o 1100

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 1102  df-3an 1103

This theorem is referenced by:  3jaodan  1456  3jaaoOLD  1459  fntpb  7208  dfwe2  7772  poseq  8153  smo11  8350  smoord  8351  omeulem1  8566  omopth2  8568  oaabs2  8634  elfiun  9389  r111  9746  r1pwss  9755  pwcfsdom  10567  winalim2  10680  xmullem  13289  xmulasslem  13310  xlemul1a  13313  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  fvf1tp  13821  symgvalstruct  19466  ordtbas2  23316  ordtbas  23317  fmfnfmlem4  24082  dyadmbl  25727  scvxcvx  27115  perfectlem2  27359  2sq2  27562  ostth3  27767  ltssolem1  27804  addsproplem7  28133  negsproplem7  28192  mulsproplem5  28278  mulsproplem6  28279  mulsproplem7  28280  mulsproplem8  28281  satfun  35801  lineext  36466  fscgr  36470  colinbtwnle  36508  broutsideof2  36512  lineunray  36537  lineelsb2  36538  elicc3  36716  4atlem11  40272  dalawlem10  40543  3cubeslem1  43306  dflim5  43947  omabs2  43950  omcl3g  43952  naddwordnexlem4  44019  frege129d  44380  goldbachth  48187  perfectALTVlem2  48375  gpgiedgdmellem  48699  gpgusgralem  48709  gpgvtxedg0  48716  gpgvtxedg1  48717  gpgedgiov  48718  gpgedg2ov  48719  gpgedg2iv  48720  gpgnbgrvtx0  48727  gpgnbgrvtx1  48728  pgnioedg1  48761  pgnioedg2  48762  pgnioedg3  48763  pgnioedg4  48764  pgnioedg5  48765  pgnbgreunbgrlem1  48766  pgnbgreunbgrlem2  48770  pgnbgreunbgrlem4  48772  pgnbgreunbgrlem5lem1  48773  pgnbgreunbgrlem5lem2  48774  pgnbgreunbgrlem5lem3  48775  pgnbgreunbgrlem5  48776  eenglngeehlnmlem1  49401  eenglngeehlnmlem2  49402