Theorem 3jaod 1431

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

Syntax hints:   → wi 4   ∨ w3o 1085

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 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaodan  1433  3jaao  1435  fntpb  7153  dfwe2  7717  poseq  8098  smo11  8294  smoord  8295  omeulem1  8507  omopth2  8509  oaabs2  8575  elfiun  9331  r111  9685  r1pwss  9694  pwcfsdom  10492  winalim2  10605  xmullem  13177  xmulasslem  13198  xlemul1a  13201  xrsupsslem  13220  xrinfmsslem  13221  xrub  13225  fvf1tp  13707  symgvalstruct  19324  ordtbas2  23133  ordtbas  23134  fmfnfmlem4  23899  dyadmbl  25555  scvxcvx  26950  perfectlem2  27195  2sq2  27398  ostth3  27603  sltsolem1  27641  addsproplem7  27945  negsproplem7  28003  mulsproplem5  28089  mulsproplem6  28090  mulsproplem7  28091  mulsproplem8  28092  satfun  35554  lineext  36219  fscgr  36223  colinbtwnle  36261  broutsideof2  36265  lineunray  36290  lineelsb2  36291  elicc3  36460  4atlem11  39808  dalawlem10  40079  3cubeslem1  42868  dflim5  43513  omabs2  43516  omcl3g  43518  naddwordnexlem4  43585  frege129d  43946  goldbachth  47735  perfectALTVlem2  47910  gpgiedgdmellem  48234  gpgusgralem  48244  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgedgiov  48253  gpgedg2ov  48254  gpgedg2iv  48255  gpgnbgrvtx0  48262  gpgnbgrvtx1  48263  pgnioedg1  48296  pgnioedg2  48297  pgnioedg3  48298  pgnioedg4  48299  pgnioedg5  48300  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem2  48305  pgnbgreunbgrlem4  48307  pgnbgreunbgrlem5lem1  48308  pgnbgreunbgrlem5lem2  48309  pgnbgreunbgrlem5lem3  48310  pgnbgreunbgrlem5  48311  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926