Theorem 3jaod 1427

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 1424	. 2 ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜒) ∧ (𝜏 → 𝜒)) → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
5	1, 2, 3, 4	syl3anc 1370	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 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaodan  1429  3jaao  1432  fntpb  7085  dfwe2  7624  smo11  8195  smoord  8196  omeulem1  8413  omopth2  8415  oaabs2  8479  elfiun  9189  r111  9533  r1pwss  9542  pwcfsdom  10339  winalim2  10452  xmullem  12998  xmulasslem  13019  xlemul1a  13022  xrsupsslem  13041  xrinfmsslem  13042  xrub  13046  symgvalstruct  19004  symgvalstructOLD  19005  ordtbas2  22342  ordtbas  22343  fmfnfmlem4  23108  dyadmbl  24764  scvxcvx  26135  perfectlem2  26378  2sq2  26581  ostth3  26786  satfun  33373  poseq  33802  sltsolem1  33878  lineext  34378  fscgr  34382  colinbtwnle  34420  broutsideof2  34424  lineunray  34449  lineelsb2  34450  elicc3  34506  4atlem11  37623  dalawlem10  37894  3cubeslem1  40506  frege129d  41371  goldbachth  44999  perfectALTVlem2  45174  eenglngeehlnmlem1  46083  eenglngeehlnmlem2  46084