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  7165  dfwe2  7730  poseq  8114  smo11  8310  smoord  8311  omeulem1  8523  omopth2  8525  oaabs2  8590  elfiun  9357  r111  9704  r1pwss  9713  pwcfsdom  10512  winalim2  10625  xmullem  13200  xmulasslem  13221  xlemul1a  13224  xrsupsslem  13243  xrinfmsslem  13244  xrub  13248  fvf1tp  13727  symgvalstruct  19311  ordtbas2  23111  ordtbas  23112  fmfnfmlem4  23877  dyadmbl  25534  scvxcvx  26929  perfectlem2  27174  2sq2  27377  ostth3  27582  sltsolem1  27620  addsproplem7  27922  negsproplem7  27980  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  satfun  35391  lineext  36057  fscgr  36061  colinbtwnle  36099  broutsideof2  36103  lineunray  36128  lineelsb2  36129  elicc3  36298  4atlem11  39596  dalawlem10  39867  3cubeslem1  42665  dflim5  43311  omabs2  43314  omcl3g  43316  naddwordnexlem4  43383  frege129d  43745  goldbachth  47541  perfectALTVlem2  47716  gpgiedgdmellem  48030  gpgusgralem  48040  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgedgiov  48049  gpgedg2ov  48050  gpgedg2iv  48051  gpgnbgrvtx0  48058  gpgnbgrvtx1  48059  pgnioedg1  48091  pgnioedg2  48092  pgnioedg3  48093  pgnioedg4  48094  pgnioedg5  48095  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem2  48100  pgnbgreunbgrlem4  48102  pgnbgreunbgrlem5lem1  48103  pgnbgreunbgrlem5lem2  48104  pgnbgreunbgrlem5lem3  48105  pgnbgreunbgrlem5  48106  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720