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  7164  dfwe2  7728  poseq  8108  smo11  8304  smoord  8305  omeulem1  8517  omopth2  8519  oaabs2  8585  elfiun  9343  r111  9699  r1pwss  9708  pwcfsdom  10506  winalim2  10619  xmullem  13216  xmulasslem  13237  xlemul1a  13240  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  fvf1tp  13748  symgvalstruct  19372  ordtbas2  23156  ordtbas  23157  fmfnfmlem4  23922  dyadmbl  25567  scvxcvx  26949  perfectlem2  27193  2sq2  27396  ostth3  27601  ltssolem1  27639  addsproplem7  27967  negsproplem7  28026  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  satfun  35593  lineext  36258  fscgr  36262  colinbtwnle  36300  broutsideof2  36304  lineunray  36329  lineelsb2  36330  elicc3  36499  4atlem11  40055  dalawlem10  40326  3cubeslem1  43116  dflim5  43757  omabs2  43760  omcl3g  43762  naddwordnexlem4  43829  frege129d  44190  goldbachth  48010  perfectALTVlem2  48198  gpgiedgdmellem  48522  gpgusgralem  48532  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem5  48599  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214