Theorem 3jaoi 1427

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 1338	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1424	. 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  1429  tpres  7221  ordzsl  7866  onzsl  7867  tfrlem16  8432  oawordeulem  8591  fsetexb  8903  elfiun  9468  infsupprpr  9542  domtriomlem  10480  axdc3lem2  10489  rankcf  10815  znegcl  12650  xrltnr  13159  xnegcl  13252  xnegneg  13253  xltnegi  13255  xnegid  13277  xaddrid  13280  xmulrid  13318  xrsupsslem  13346  xrinfmsslem  13347  reltxrnmnf  13381  elfznelfzo  13808  addmodlteq  13984  hashle2pr  14513  hashge2el2difr  14517  hashtpg  14521  hash1to3  14528  hash3tpde  14529  swrdnd0  14692  prm23lt5  16848  prm23ge5  16849  cshwshashlem1  17130  01eq0ringOLD  20548  ioombl1  25611  2irrexpq  26788  ppiublem1  27261  zabsle1  27355  gausslemma2dlem0f  27420  gausslemma2dlem0i  27423  gausslemma2dlem4  27428  2lgsoddprm  27475  ostth  27698  sltval2  27716  sltintdifex  27721  sltres  27722  sltsolem1  27735  nosepnelem  27739  nb3grprlem1  29412  pthdivtx  29762  frgr3vlem1  30302  frgr3vlem2  30303  frgrwopreg  30352  frgrregorufr  30354  frgrregord13  30425  kur14lem7  35197  3jaodd  35695  dfrdg2  35777  dfrdg4  35933  iooelexlt  37345  relowlssretop  37346  wl-exeq  37515  iccpartiltu  47347  iccpartigtl  47348  icceuelpart  47361  prproropf1olem4  47431  fmtno4prmfac193  47498  fmtnofz04prm  47502  mogoldbblem  47645  grtriproplem  47844  grtrif1o  47847  exple2lt6  48209