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  7214  dfwe2  7779  poseq  8160  smo11  8357  smoord  8358  omeulem1  8573  omopth2  8575  oaabs2  8641  elfiun  9397  r111  9754  r1pwss  9763  pwcfsdom  10585  winalim2  10698  xmullem  13308  xmulasslem  13329  xlemul1a  13332  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  fvf1tp  13842  symgvalstruct  19513  ordtbas2  23400  ordtbas  23401  fmfnfmlem4  24167  dyadmbl  25812  scvxcvx  27203  perfectlem2  27447  2sq2  27650  ostth3  27855  ltssolem1  27892  addsproplem7  28221  negsproplem7  28280  mulsproplem5  28366  mulsproplem6  28367  mulsproplem7  28368  mulsproplem8  28369  satfun  35942  lineext  36607  fscgr  36611  colinbtwnle  36649  broutsideof2  36653  lineunray  36678  lineelsb2  36679  elicc3  36887  4atlem11  40443  dalawlem10  40714  3cubeslem1  43475  dflim5  44116  omabs2  44119  omcl3g  44121  naddwordnexlem4  44188  frege129d  44549  goldbachth  48359  perfectALTVlem2  48547  gpgiedgdmellem  48871  gpgusgralem  48881  gpgvtxedg0  48888  gpgvtxedg1  48889  gpgedgiov  48890  gpgedg2ov  48891  gpgedg2iv  48892  gpgnbgrvtx0  48899  gpgnbgrvtx1  48900  pgnioedg1  48933  pgnioedg2  48934  pgnioedg3  48935  pgnioedg4  48936  pgnioedg5  48937  pgnbgreunbgrlem1  48938  pgnbgreunbgrlem2  48942  pgnbgreunbgrlem4  48944  pgnbgreunbgrlem5lem1  48945  pgnbgreunbgrlem5lem2  48946  pgnbgreunbgrlem5lem3  48947  pgnbgreunbgrlem5  48948  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577