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  19303  ordtbas2  23054  ordtbas  23055  fmfnfmlem4  23820  dyadmbl  25477  scvxcvx  26872  perfectlem2  27117  2sq2  27320  ostth3  27525  sltsolem1  27563  addsproplem7  27858  negsproplem7  27916  mulsproplem5  27999  mulsproplem6  28000  mulsproplem7  28001  mulsproplem8  28002  satfun  35371  lineext  36037  fscgr  36041  colinbtwnle  36079  broutsideof2  36083  lineunray  36108  lineelsb2  36109  elicc3  36278  4atlem11  39576  dalawlem10  39847  3cubeslem1  42645  dflim5  43291  omabs2  43294  omcl3g  43296  naddwordnexlem4  43363  frege129d  43725  goldbachth  47521  perfectALTVlem2  47696  gpgiedgdmellem  48010  gpgusgralem  48020  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  gpgnbgrvtx0  48038  gpgnbgrvtx1  48039  pgnioedg1  48071  pgnioedg2  48072  pgnioedg3  48073  pgnioedg4  48074  pgnioedg5  48075  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  pgnbgreunbgrlem5  48086  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700