Theorem 3jaoi 1429

Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.)

Hypotheses

Ref	Expression
3jaoi.1	⊢ (𝜑 → 𝜓)
3jaoi.2	⊢ (𝜒 → 𝜓)
3jaoi.3	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
3jaoi	⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Proof of Theorem 3jaoi

Step	Hyp	Ref	Expression
1		3jaoi.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3		3jaoi.3	. . 3 ⊢ (𝜃 → 𝜓)
4	1, 2, 3	3pm3.2i 1339	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1426	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∨ w3o 1085   ∧ w3a 1086

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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaoian  1431  tpres  7189  ordzsl  7834  onzsl  7835  tfrlem16  8401  oawordeulem  8560  fsetexb  8872  elfiun  9436  infsupprpr  9510  domtriomlem  10448  axdc3lem2  10457  rankcf  10783  znegcl  12619  xrltnr  13127  xnegcl  13221  xnegneg  13222  xltnegi  13224  xnegid  13246  xaddrid  13249  xmulrid  13287  xrsupsslem  13315  xrinfmsslem  13316  reltxrnmnf  13350  elfznelfzo  13777  addmodlteq  13953  hashle2pr  14483  hashge2el2difr  14487  hashtpg  14491  hash1to3  14498  hash3tpde  14499  swrdnd0  14662  prm23lt5  16819  prm23ge5  16820  cshwshashlem1  17100  01eq0ringOLD  20476  ioombl1  25500  2irrexpq  26676  ppiublem1  27149  zabsle1  27243  gausslemma2dlem0f  27308  gausslemma2dlem0i  27311  gausslemma2dlem4  27316  2lgsoddprm  27363  ostth  27586  sltval2  27604  sltintdifex  27609  sltres  27610  sltsolem1  27623  nosepnelem  27627  nb3grprlem1  29291  pthdivtx  29641  frgr3vlem1  30186  frgr3vlem2  30187  frgrwopreg  30236  frgrregorufr  30238  frgrregord13  30309  kur14lem7  35155  3jaodd  35653  dfrdg2  35734  dfrdg4  35890  iooelexlt  37301  relowlssretop  37302  wl-exeq  37473  iccpartiltu  47354  iccpartigtl  47355  icceuelpart  47368  prproropf1olem4  47438  fmtno4prmfac193  47505  fmtnofz04prm  47509  mogoldbblem  47652  grtriproplem  47851  grtrif1o  47854  exple2lt6  48225