Theorem 3jaod 1431

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

This theorem is referenced by:  3jaodan  1433  3jaao  1435  fntpb  7229  dfwe2  7794  poseq  8183  smo11  8404  smoord  8405  omeulem1  8620  omopth2  8622  oaabs2  8687  elfiun  9470  r111  9815  r1pwss  9824  pwcfsdom  10623  winalim2  10736  xmullem  13306  xmulasslem  13327  xlemul1a  13330  xrsupsslem  13349  xrinfmsslem  13350  xrub  13354  fvf1tp  13829  symgvalstruct  19414  symgvalstructOLD  19415  ordtbas2  23199  ordtbas  23200  fmfnfmlem4  23965  dyadmbl  25635  scvxcvx  27029  perfectlem2  27274  2sq2  27477  ostth3  27682  sltsolem1  27720  addsproplem7  28008  negsproplem7  28066  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  satfun  35416  lineext  36077  fscgr  36081  colinbtwnle  36119  broutsideof2  36123  lineunray  36148  lineelsb2  36149  elicc3  36318  4atlem11  39611  dalawlem10  39882  3cubeslem1  42695  dflim5  43342  omabs2  43345  omcl3g  43347  naddwordnexlem4  43414  frege129d  43776  goldbachth  47534  perfectALTVlem2  47709  gpgedgel  48007  gpgusgralem  48011  gpgvtxedg0  48021  gpgvtxedg1  48022  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659