Theorem 3jaod 1457

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 1453	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1399	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  1459  3jaaoOLD  1462  fntpb  7246  dfwe2  7820  poseq  8212  smo11  8410  smoord  8411  omeulem1  8628  omopth2  8630  oaabs2  8696  elfiun  9459  r111  9819  r1pwss  9828  pwcfsdom  10707  winalim2  10820  xmullem  13434  xmulasslem  13455  xlemul1a  13458  xrsupsslem  13477  xrinfmsslem  13478  xrub  13482  fvf1tp  13969  symgvalstruct  19662  ordtbas2  23564  ordtbas  23565  fmfnfmlem4  24331  dyadmbl  25976  scvxcvx  27370  perfectlem2  27614  2sq2  27817  ostth3  28022  ltssolem1  28089  addsproplem7  28418  negsproplem7  28477  mulsproplem5  28563  mulsproplem6  28564  mulsproplem7  28565  mulsproplem8  28566  satfun  36384  lineext  37056  fscgr  37060  colinbtwnle  37098  broutsideof2  37102  lineunray  37127  lineelsb2  37128  elicc3  37320  4atlem11  40932  dalawlem10  41203  3cubeslem1  43960  dflim5  44592  omabs2  44595  omcl3g  44597  naddwordnexlem4  44664  frege129d  45024  goldbachth  48905  perfectALTVlem2  49093  gpgiedgdmellem  49417  gpgusgralem  49427  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgedgiov  49436  gpgedg2ov  49437  gpgedg2iv  49438  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5lem1  49491  pgnbgreunbgrlem5lem2  49492  pgnbgreunbgrlem5lem3  49493  pgnbgreunbgrlem5  49494  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182