Theorem 3jaod 1426

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

Syntax hints:   → wi 4   ∨ w3o 1084

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 396  df-or 844  df-3or 1086  df-3an 1087

This theorem is referenced by:  3jaodan  1428  3jaao  1431  fntpb  7067  dfwe2  7602  smo11  8166  smoord  8167  omeulem1  8375  omopth2  8377  oaabs2  8439  elfiun  9119  r111  9464  r1pwss  9473  pwcfsdom  10270  winalim2  10383  xmullem  12927  xmulasslem  12948  xlemul1a  12951  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  symgvalstruct  18919  symgvalstructOLD  18920  ordtbas2  22250  ordtbas  22251  fmfnfmlem4  23016  dyadmbl  24669  scvxcvx  26040  perfectlem2  26283  2sq2  26486  ostth3  26691  satfun  33273  poseq  33729  sltsolem1  33805  lineext  34305  fscgr  34309  colinbtwnle  34347  broutsideof2  34351  lineunray  34376  lineelsb2  34377  elicc3  34433  4atlem11  37550  dalawlem10  37821  3cubeslem1  40422  frege129d  41260  goldbachth  44887  perfectALTVlem2  45062  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972