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

Syntax hints:   → wi 4   ∨ w3o 1087

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 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090

This theorem is referenced by:  3jaodan  1431  3jaao  1434  fntpb  7211  dfwe2  7761  poseq  8144  smo11  8364  smoord  8365  omeulem1  8582  omopth2  8584  oaabs2  8648  elfiun  9425  r111  9770  r1pwss  9779  pwcfsdom  10578  winalim2  10691  xmullem  13243  xmulasslem  13264  xlemul1a  13267  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  symgvalstruct  19264  symgvalstructOLD  19265  ordtbas2  22695  ordtbas  22696  fmfnfmlem4  23461  dyadmbl  25117  scvxcvx  26490  perfectlem2  26733  2sq2  26936  ostth3  27141  sltsolem1  27178  addsproplem7  27459  negsproplem7  27508  mulsproplem5  27576  mulsproplem6  27577  mulsproplem7  27578  mulsproplem8  27579  satfun  34402  lineext  35048  fscgr  35052  colinbtwnle  35090  broutsideof2  35094  lineunray  35119  lineelsb2  35120  elicc3  35202  4atlem11  38480  dalawlem10  38751  3cubeslem1  41422  dflim5  42079  omabs2  42082  omcl3g  42084  naddwordnexlem4  42152  frege129d  42514  goldbachth  46215  perfectALTVlem2  46390  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424