Theorem 3jaod 1425

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

Syntax hints:   → wi 4   ∨ w3o 1083

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 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086

This theorem is referenced by:  3jaodan  1427  3jaao  1430  fntpb  6949  dfwe2  7476  smo11  7984  smoord  7985  omeulem1  8191  omopth2  8193  oaabs2  8255  elfiun  8878  r111  9188  r1pwss  9197  pwcfsdom  9994  winalim2  10107  xmullem  12645  xmulasslem  12666  xlemul1a  12669  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  symgvalstruct  18517  ordtbas2  21796  ordtbas  21797  fmfnfmlem4  22562  dyadmbl  24204  scvxcvx  25571  perfectlem2  25814  2sq2  26017  ostth3  26222  satfun  32771  poseq  33208  sltsolem1  33293  lineext  33650  fscgr  33654  colinbtwnle  33692  broutsideof2  33696  lineunray  33721  lineelsb2  33722  elicc3  33778  4atlem11  36905  dalawlem10  37176  3cubeslem1  39625  frege129d  40464  goldbachth  44064  perfectALTVlem2  44240  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152