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  7145  dfwe2  7710  poseq  8091  smo11  8287  smoord  8288  omeulem1  8500  omopth2  8502  oaabs2  8567  elfiun  9320  r111  9671  r1pwss  9680  pwcfsdom  10477  winalim2  10590  xmullem  13166  xmulasslem  13187  xlemul1a  13190  xrsupsslem  13209  xrinfmsslem  13210  xrub  13214  fvf1tp  13693  symgvalstruct  19276  ordtbas2  23076  ordtbas  23077  fmfnfmlem4  23842  dyadmbl  25499  scvxcvx  26894  perfectlem2  27139  2sq2  27342  ostth3  27547  sltsolem1  27585  addsproplem7  27887  negsproplem7  27945  mulsproplem5  28028  mulsproplem6  28029  mulsproplem7  28030  mulsproplem8  28031  satfun  35388  lineext  36054  fscgr  36058  colinbtwnle  36096  broutsideof2  36100  lineunray  36125  lineelsb2  36126  elicc3  36295  4atlem11  39592  dalawlem10  39863  3cubeslem1  42661  dflim5  43306  omabs2  43309  omcl3g  43311  naddwordnexlem4  43378  frege129d  43740  goldbachth  47535  perfectALTVlem2  47710  gpgiedgdmellem  48034  gpgusgralem  48044  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgedgiov  48053  gpgedg2ov  48054  gpgedg2iv  48055  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  pgnioedg1  48096  pgnioedg2  48097  pgnioedg3  48098  pgnioedg4  48099  pgnioedg5  48100  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5lem1  48108  pgnbgreunbgrlem5lem2  48109  pgnbgreunbgrlem5lem3  48110  pgnbgreunbgrlem5  48111  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727