Theorem 3jaod 1449

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

Syntax hints:   → wi 4   ∨ w3o 1097

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 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100

This theorem is referenced by:  3jaodan  1451  3jaaoOLD  1454  fntpb  7193  dfwe2  7757  poseq  8138  smo11  8335  smoord  8336  omeulem1  8551  omopth2  8553  oaabs2  8619  elfiun  9376  r111  9733  r1pwss  9742  pwcfsdom  10541  winalim2  10654  xmullem  13267  xmulasslem  13288  xlemul1a  13291  xrsupsslem  13310  xrinfmsslem  13311  xrub  13315  fvf1tp  13799  symgvalstruct  19437  ordtbas2  23251  ordtbas  23252  fmfnfmlem4  24017  dyadmbl  25662  scvxcvx  27050  perfectlem2  27294  2sq2  27497  ostth3  27702  ltssolem1  27739  addsproplem7  28068  negsproplem7  28127  mulsproplem5  28213  mulsproplem6  28214  mulsproplem7  28215  mulsproplem8  28216  satfun  35761  lineext  36426  fscgr  36430  colinbtwnle  36468  broutsideof2  36472  lineunray  36497  lineelsb2  36498  elicc3  36677  4atlem11  40233  dalawlem10  40504  3cubeslem1  43265  dflim5  43906  omabs2  43909  omcl3g  43911  naddwordnexlem4  43978  frege129d  44339  goldbachth  48156  perfectALTVlem2  48344  gpgiedgdmellem  48668  gpgusgralem  48678  gpgvtxedg0  48685  gpgvtxedg1  48686  gpgedgiov  48687  gpgedg2ov  48688  gpgedg2iv  48689  gpgnbgrvtx0  48696  gpgnbgrvtx1  48697  pgnioedg1  48730  pgnioedg2  48731  pgnioedg3  48732  pgnioedg4  48733  pgnioedg5  48734  pgnbgreunbgrlem1  48735  pgnbgreunbgrlem2  48739  pgnbgreunbgrlem4  48741  pgnbgreunbgrlem5lem1  48742  pgnbgreunbgrlem5lem2  48743  pgnbgreunbgrlem5lem3  48744  pgnbgreunbgrlem5  48745  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360