Theorem 3jaod 1432

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

Syntax hints:   → wi 4   ∨ w3o 1086

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 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaodan  1434  3jaao  1436  fntpb  7158  dfwe2  7722  poseq  8102  smo11  8298  smoord  8299  omeulem1  8511  omopth2  8513  oaabs2  8579  elfiun  9337  r111  9693  r1pwss  9702  pwcfsdom  10500  winalim2  10613  xmullem  13210  xmulasslem  13231  xlemul1a  13234  xrsupsslem  13253  xrinfmsslem  13254  xrub  13258  fvf1tp  13742  symgvalstruct  19366  ordtbas2  23169  ordtbas  23170  fmfnfmlem4  23935  dyadmbl  25580  scvxcvx  26966  perfectlem2  27210  2sq2  27413  ostth3  27618  ltssolem1  27656  addsproplem7  27984  negsproplem7  28043  mulsproplem5  28129  mulsproplem6  28130  mulsproplem7  28131  mulsproplem8  28132  satfun  35612  lineext  36277  fscgr  36281  colinbtwnle  36319  broutsideof2  36323  lineunray  36348  lineelsb2  36349  elicc3  36518  4atlem11  40072  dalawlem10  40343  3cubeslem1  43133  dflim5  43778  omabs2  43781  omcl3g  43783  naddwordnexlem4  43850  frege129d  44211  goldbachth  48025  perfectALTVlem2  48213  gpgiedgdmellem  48537  gpgusgralem  48547  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  gpgnbgrvtx0  48565  gpgnbgrvtx1  48566  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  pgnbgreunbgrlem5  48614  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229