Theorem 3jaod 1384

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

Syntax hints:   → wi 4   ∨ w3o 1030

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 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033

This theorem is referenced by:  3jaodan  1386  3jaao  1388  fntpb  6378  dfwe2  6873  smo11  7348  smoord  7349  omeulem1  7549  omopth2  7551  oaabs2  7612  elfiun  8219  r111  8521  r1pwss  8530  pwcfsdom  9284  winalim2  9397  xmullem  11966  xmulasslem  11987  xlemul1a  11990  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  ordtbas2  20805  ordtbas  20806  fmfnfmlem4  21571  dyadmbl  23174  scvxcvx  24512  perfectlem2  24755  ostth3  25127  poseq  30994  sltsolem1  31067  lineext  31353  fscgr  31357  colinbtwnle  31395  broutsideof2  31399  lineunray  31424  lineelsb2  31425  elicc3  31481  4atlem11  33913  dalawlem10  34184  frege129d  37074  goldbachth  39997  perfectALTVlem2  40165