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  7183  dfwe2  7750  poseq  8137  smo11  8333  smoord  8334  omeulem1  8546  omopth2  8548  oaabs2  8613  elfiun  9381  r111  9728  r1pwss  9737  pwcfsdom  10536  winalim2  10649  xmullem  13224  xmulasslem  13245  xlemul1a  13248  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  fvf1tp  13751  symgvalstruct  19327  ordtbas2  23078  ordtbas  23079  fmfnfmlem4  23844  dyadmbl  25501  scvxcvx  26896  perfectlem2  27141  2sq2  27344  ostth3  27549  sltsolem1  27587  addsproplem7  27882  negsproplem7  27940  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  satfun  35398  lineext  36064  fscgr  36068  colinbtwnle  36106  broutsideof2  36110  lineunray  36135  lineelsb2  36136  elicc3  36305  4atlem11  39603  dalawlem10  39874  3cubeslem1  42672  dflim5  43318  omabs2  43321  omcl3g  43323  naddwordnexlem4  43390  frege129d  43752  goldbachth  47548  perfectALTVlem2  47723  gpgiedgdmellem  48037  gpgusgralem  48047  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem5  48113  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727