Theorem 3jaod 1437

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

Syntax hints:   → wi 4   ∨ w3o 1091

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 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094

This theorem is referenced by:  3jaodan  1439  3jaao  1441  fntpb  7153  dfwe2  7717  poseq  8098  smo11  8294  smoord  8295  omeulem1  8507  omopth2  8509  oaabs2  8575  elfiun  9333  r111  9690  r1pwss  9699  pwcfsdom  10497  winalim2  10610  xmullem  13207  xmulasslem  13228  xlemul1a  13231  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  fvf1tp  13739  symgvalstruct  19363  ordtbas2  23174  ordtbas  23175  fmfnfmlem4  23940  dyadmbl  25585  scvxcvx  26967  perfectlem2  27211  2sq2  27414  ostth3  27619  ltssolem1  27657  addsproplem7  27985  negsproplem7  28044  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  satfun  35639  lineext  36304  fscgr  36308  colinbtwnle  36346  broutsideof2  36350  lineunray  36375  lineelsb2  36376  elicc3  36545  4atlem11  40101  dalawlem10  40372  3cubeslem1  43133  dflim5  43774  omabs2  43777  omcl3g  43779  naddwordnexlem4  43846  frege129d  44207  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