Theorem 3jaoi 1430

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 1340	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1427	. 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  1432  tpres  7135  ordzsl  7775  onzsl  7776  tfrlem16  8312  oawordeulem  8469  fsetexb  8788  elfiun  9314  infsupprpr  9390  domtriomlem  10333  axdc3lem2  10342  rankcf  10668  znegcl  12507  xrltnr  13018  xnegcl  13112  xnegneg  13113  xltnegi  13115  xnegid  13137  xaddrid  13140  xmulrid  13178  xrsupsslem  13206  xrinfmsslem  13207  reltxrnmnf  13242  elfznelfzo  13673  addmodlteq  13853  hashle2pr  14384  hashge2el2difr  14388  hashtpg  14392  hash1to3  14399  hash3tpde  14400  swrdnd0  14565  prm23lt5  16726  prm23ge5  16727  cshwshashlem1  17007  01eq0ringOLD  20446  ioombl1  25490  2irrexpq  26667  ppiublem1  27140  zabsle1  27234  gausslemma2dlem0f  27299  gausslemma2dlem0i  27302  gausslemma2dlem4  27307  2lgsoddprm  27354  ostth  27577  sltval2  27595  sltintdifex  27600  sltres  27601  sltsolem1  27614  nosepnelem  27618  nb3grprlem1  29358  pthdivtx  29705  frgr3vlem1  30253  frgr3vlem2  30254  frgrwopreg  30303  frgrregorufr  30305  frgrregord13  30376  kur14lem7  35256  3jaodd  35759  dfrdg2  35837  dfrdg4  35995  iooelexlt  37406  relowlssretop  37407  wl-exeq  37578  iccpartiltu  47521  iccpartigtl  47522  icceuelpart  47535  prproropf1olem4  47605  fmtno4prmfac193  47672  fmtnofz04prm  47676  mogoldbblem  47819  grtriproplem  48038  grtrif1o  48041  gpgprismgr4cycllem7  48200  pgnbgreunbgrlem1  48212  pgnbgreunbgrlem2lem1  48213  pgnbgreunbgrlem2lem2  48214  pgnbgreunbgrlem2lem3  48215  pgnbgreunbgrlem2  48216  pgnbgreunbgrlem4  48218  pgnbgreunbgrlem5  48222  exple2lt6  48463