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 1085

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 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaodan  1433  3jaao  1435  fntpb  7201  dfwe2  7768  poseq  8157  smo11  8378  smoord  8379  omeulem1  8594  omopth2  8596  oaabs2  8661  elfiun  9442  r111  9789  r1pwss  9798  pwcfsdom  10597  winalim2  10710  xmullem  13280  xmulasslem  13301  xlemul1a  13304  xrsupsslem  13323  xrinfmsslem  13324  xrub  13328  fvf1tp  13806  symgvalstruct  19378  ordtbas2  23129  ordtbas  23130  fmfnfmlem4  23895  dyadmbl  25553  scvxcvx  26948  perfectlem2  27193  2sq2  27396  ostth3  27601  sltsolem1  27639  addsproplem7  27934  negsproplem7  27992  mulsproplem5  28075  mulsproplem6  28076  mulsproplem7  28077  mulsproplem8  28078  satfun  35433  lineext  36094  fscgr  36098  colinbtwnle  36136  broutsideof2  36140  lineunray  36165  lineelsb2  36166  elicc3  36335  4atlem11  39628  dalawlem10  39899  3cubeslem1  42707  dflim5  43353  omabs2  43356  omcl3g  43358  naddwordnexlem4  43425  frege129d  43787  goldbachth  47561  perfectALTVlem2  47736  gpgiedgdmellem  48050  gpgusgralem  48060  gpgvtxedg0  48067  gpgvtxedg1  48068  gpgnbgrvtx0  48076  gpgnbgrvtx1  48077  eenglngeehlnmlem1  48717  eenglngeehlnmlem2  48718