Theorem 3jaod 1429

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 1425	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1371	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 847  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaodan  1431  3jaao  1433  fntpb  7246  dfwe2  7809  poseq  8199  smo11  8420  smoord  8421  omeulem1  8638  omopth2  8640  oaabs2  8705  elfiun  9499  r111  9844  r1pwss  9853  pwcfsdom  10652  winalim2  10765  xmullem  13326  xmulasslem  13347  xlemul1a  13350  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  fvf1tp  13840  symgvalstruct  19438  symgvalstructOLD  19439  ordtbas2  23220  ordtbas  23221  fmfnfmlem4  23986  dyadmbl  25654  scvxcvx  27047  perfectlem2  27292  2sq2  27495  ostth3  27700  sltsolem1  27738  addsproplem7  28026  negsproplem7  28084  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  satfun  35379  lineext  36040  fscgr  36044  colinbtwnle  36082  broutsideof2  36086  lineunray  36111  lineelsb2  36112  elicc3  36283  4atlem11  39566  dalawlem10  39837  3cubeslem1  42640  dflim5  43291  omabs2  43294  omcl3g  43296  naddwordnexlem4  43363  frege129d  43725  goldbachth  47421  perfectALTVlem2  47596  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472