Theorem 3jaod 1424

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

Syntax hints:   → wi 4   ∨ w3o 1082

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 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085

This theorem is referenced by:  3jaodan  1426  3jaao  1429  fntpb  6953  dfwe2  7477  smo11  7982  smoord  7983  omeulem1  8189  omopth2  8191  oaabs2  8253  elfiun  8875  r111  9185  r1pwss  9194  pwcfsdom  9986  winalim2  10099  xmullem  12639  xmulasslem  12660  xlemul1a  12663  xrsupsslem  12682  xrinfmsslem  12683  xrub  12687  symgvalstruct  18503  ordtbas2  21777  ordtbas  21778  fmfnfmlem4  22543  dyadmbl  24179  scvxcvx  25544  perfectlem2  25787  2sq2  25990  ostth3  26195  satfun  32660  poseq  33097  sltsolem1  33182  lineext  33539  fscgr  33543  colinbtwnle  33581  broutsideof2  33585  lineunray  33610  lineelsb2  33611  elicc3  33667  4atlem11  36772  dalawlem10  37043  3cubeslem1  39368  frege129d  40193  goldbachth  43789  perfectALTVlem2  43967  eenglngeehlnmlem1  44804  eenglngeehlnmlem2  44805