Theorem 3jaod 1456

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105

This theorem is used by:  3jaodan  1458  3jaaoOLD  1461  fntpb  7219  dfwe2  7792  poseq  8182  smo11  8380  smoord  8381  omeulem1  8598  omopth2  8600  oaabs2  8666  elfiun  9429  r111  9789  r1pwss  9798  pwcfsdom  10675  winalim2  10788  xmullem  13401  xmulasslem  13422  xlemul1a  13425  xrsupsslem  13444  xrinfmsslem  13445  xrub  13449  fvf1tp  13936  symgvalstruct  19620  ordtbas2  23518  ordtbas  23519  fmfnfmlem4  24285  dyadmbl  25930  scvxcvx  27322  perfectlem2  27566  2sq2  27769  ostth3  27974  ltssolem1  28041  addsproplem7  28370  negsproplem7  28429  mulsproplem5  28515  mulsproplem6  28516  mulsproplem7  28517  mulsproplem8  28518  satfun  36294  lineext  36965  fscgr  36969  colinbtwnle  37007  broutsideof2  37011  lineunray  37036  lineelsb2  37037  elicc3  37229  4atlem11  40803  dalawlem10  41074  3cubeslem1  43831  dflim5  44468  omabs2  44471  omcl3g  44473  naddwordnexlem4  44540  frege129d  44900  goldbachth  48768  perfectALTVlem2  48956  gpgiedgdmellem  49280  gpgusgralem  49290  gpgvtxedg0  49297  gpgvtxedg1  49298  gpgedgiov  49299  gpgedg2ov  49300  gpgedg2iv  49301  gpgnbgrvtx0  49308  gpgnbgrvtx1  49309  pgnioedg1  49342  pgnioedg2  49343  pgnioedg3  49344  pgnioedg4  49345  pgnioedg5  49346  pgnbgreunbgrlem1  49347  pgnbgreunbgrlem2  49351  pgnbgreunbgrlem4  49353  pgnbgreunbgrlem5lem1  49354  pgnbgreunbgrlem5lem2  49355  pgnbgreunbgrlem5lem3  49356  pgnbgreunbgrlem5  49357  eenglngeehlnmlem1  49986  eenglngeehlnmlem2  49987