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  7215  dfwe2  7788  poseq  8175  smo11  8372  smoord  8373  omeulem1  8590  omopth2  8592  oaabs2  8658  elfiun  9422  r111  9782  r1pwss  9791  pwcfsdom  10668  winalim2  10781  xmullem  13394  xmulasslem  13415  xlemul1a  13418  xrsupsslem  13437  xrinfmsslem  13438  xrub  13442  fvf1tp  13929  symgvalstruct  19611  ordtbas2  23509  ordtbas  23510  fmfnfmlem4  24276  dyadmbl  25921  scvxcvx  27313  perfectlem2  27557  2sq2  27760  ostth3  27965  ltssolem1  28032  addsproplem7  28361  negsproplem7  28420  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  satfun  36176  lineext  36841  fscgr  36845  colinbtwnle  36883  broutsideof2  36887  lineunray  36912  lineelsb2  36913  elicc3  37105  4atlem11  40666  dalawlem10  40937  3cubeslem1  43694  dflim5  44330  omabs2  44333  omcl3g  44335  naddwordnexlem4  44402  frege129d  44762  goldbachth  48631  perfectALTVlem2  48819  gpgiedgdmellem  49143  gpgusgralem  49153  gpgvtxedg0  49160  gpgvtxedg1  49161  gpgedgiov  49162  gpgedg2ov  49163  gpgedg2iv  49164  gpgnbgrvtx0  49171  gpgnbgrvtx1  49172  pgnioedg1  49205  pgnioedg2  49206  pgnioedg3  49207  pgnioedg4  49208  pgnioedg5  49209  pgnbgreunbgrlem1  49210  pgnbgreunbgrlem2  49214  pgnbgreunbgrlem4  49216  pgnbgreunbgrlem5lem1  49217  pgnbgreunbgrlem5lem2  49218  pgnbgreunbgrlem5lem3  49219  pgnbgreunbgrlem5  49220  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849