Theorem 3jaod 1432

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaodan  1434  3jaao  1436  fntpb  7165  dfwe2  7729  poseq  8110  smo11  8306  smoord  8307  omeulem1  8519  omopth2  8521  oaabs2  8587  elfiun  9345  r111  9699  r1pwss  9708  pwcfsdom  10506  winalim2  10619  xmullem  13191  xmulasslem  13212  xlemul1a  13215  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  fvf1tp  13721  symgvalstruct  19338  ordtbas2  23147  ordtbas  23148  fmfnfmlem4  23913  dyadmbl  25569  scvxcvx  26964  perfectlem2  27209  2sq2  27412  ostth3  27617  ltssolem1  27655  addsproplem7  27983  negsproplem7  28042  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  satfun  35627  lineext  36292  fscgr  36296  colinbtwnle  36334  broutsideof2  36338  lineunray  36363  lineelsb2  36364  elicc3  36533  4atlem11  39985  dalawlem10  40256  3cubeslem1  43041  dflim5  43686  omabs2  43689  omcl3g  43691  naddwordnexlem4  43758  frege129d  44119  goldbachth  47907  perfectALTVlem2  48082  gpgiedgdmellem  48406  gpgusgralem  48416  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgedgiov  48425  gpgedg2ov  48426  gpgedg2iv  48427  gpgnbgrvtx0  48434  gpgnbgrvtx1  48435  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem2  48477  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  pgnbgreunbgrlem5  48483  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098