Theorem 3jaoi 1431

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 1341	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1428	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

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

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 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaoian  1433  tpres  7156  ordzsl  7796  onzsl  7797  tfrlem16  8332  oawordeulem  8489  fsetexb  8811  elfiun  9343  infsupprpr  9419  domtriomlem  10364  axdc3lem2  10373  rankcf  10700  znegcl  12562  xrltnr  13070  xnegcl  13165  xnegneg  13166  xltnegi  13168  xnegid  13190  xaddrid  13193  xmulrid  13231  xrsupsslem  13259  xrinfmsslem  13260  reltxrnmnf  13295  elfznelfzo  13728  addmodlteq  13908  hashle2pr  14439  hashge2el2difr  14443  hashtpg  14447  hash1to3  14454  hash3tpde  14455  swrdnd0  14620  prm23lt5  16785  prm23ge5  16786  cshwshashlem1  17066  01eq0ringOLD  20508  ioombl1  25529  2irrexpq  26695  ppiublem1  27165  zabsle1  27259  gausslemma2dlem0f  27324  gausslemma2dlem0i  27327  gausslemma2dlem4  27332  2lgsoddprm  27379  ostth  27602  ltsval2  27620  ltsintdifex  27625  ltsres  27626  ltssolem1  27639  nosepnelem  27643  nb3grprlem1  29449  pthdivtx  29795  frgr3vlem1  30343  frgr3vlem2  30344  frgrwopreg  30393  frgrregorufr  30395  frgrregord13  30466  kur14lem7  35394  3jaodd  35897  dfrdg2  35975  dfrdg4  36133  iooelexlt  37678  relowlssretop  37679  wl-exeq  37859  iccpartiltu  47882  iccpartigtl  47883  icceuelpart  47896  prproropf1olem4  47966  fmtno4prmfac193  48036  fmtnofz04prm  48040  mogoldbblem  48196  grtriproplem  48415  grtrif1o  48418  gpgprismgr4cycllem7  48577  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  exple2lt6  48840