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  7209  dfwe2  7774  poseq  8157  smo11  8354  smoord  8355  omeulem1  8570  omopth2  8572  oaabs2  8638  elfiun  9401  r111  9758  r1pwss  9767  pwcfsdom  10593  winalim2  10706  xmullem  13317  xmulasslem  13338  xlemul1a  13341  xrsupsslem  13360  xrinfmsslem  13361  xrub  13365  fvf1tp  13851  symgvalstruct  19525  ordtbas2  23417  ordtbas  23418  fmfnfmlem4  24184  dyadmbl  25829  scvxcvx  27223  perfectlem2  27467  2sq2  27670  ostth3  27875  ltssolem1  27912  addsproplem7  28241  negsproplem7  28300  mulsproplem5  28386  mulsproplem6  28387  mulsproplem7  28388  mulsproplem8  28389  satfun  35991  lineext  36657  fscgr  36661  colinbtwnle  36699  broutsideof2  36703  lineunray  36728  lineelsb2  36729  elicc3  36937  4atlem11  40483  dalawlem10  40754  3cubeslem1  43530  dflim5  44171  omabs2  44174  omcl3g  44176  naddwordnexlem4  44243  frege129d  44604  goldbachth  48451  perfectALTVlem2  48639  gpgiedgdmellem  48963  gpgusgralem  48973  gpgvtxedg0  48980  gpgvtxedg1  48981  gpgedgiov  48982  gpgedg2ov  48983  gpgedg2iv  48984  gpgnbgrvtx0  48991  gpgnbgrvtx1  48992  pgnioedg1  49025  pgnioedg2  49026  pgnioedg3  49027  pgnioedg4  49028  pgnioedg5  49029  pgnbgreunbgrlem1  49030  pgnbgreunbgrlem2  49034  pgnbgreunbgrlem4  49036  pgnbgreunbgrlem5lem1  49037  pgnbgreunbgrlem5lem2  49038  pgnbgreunbgrlem5lem3  49039  pgnbgreunbgrlem5  49040  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669