Theorem 3jaoi 1454

Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.) (Proof shortened by Garrett Katz, 16-Jun-2026.)

Hypotheses

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

Assertion

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

Proof of Theorem 3jaoi

Step	Hyp	Ref	Expression
1		3jaoi.1	. 2 ⊢ (𝜑 → 𝜓)
2		3jaoi.2	. 2 ⊢ (𝜒 → 𝜓)
3		3jaoi.3	. 2 ⊢ (𝜃 → 𝜓)
4		3jaob 1453	. 2 ⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
5	1, 2, 3, 4	mpbir3an 1360	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105

This theorem is used by:  3jaoian  1457  tpres  7203  ordzsl  7847  onzsl  7848  tfrlem16  8387  oawordeulem  8548  fsetexb  8872  elfiun  9407  infsupprpr  9483  domtriomlem  10469  axdc3lem2  10478  rankcf  10811  znegcl  12678  xrltnr  13195  xnegcl  13290  xnegneg  13291  xltnegi  13293  xnegid  13315  xaddrid  13318  xmulrid  13356  xrsupsslem  13384  xrinfmsslem  13385  reltxrnmnf  13420  elfznelfzo  13854  addmodlteq  14035  hashle2pr  14567  hashge2el2difr  14571  hashtpg  14575  hash1to3  14582  hash3tpde  14583  swrdnd0  14752  prm23lt5  16931  prm23ge5  16932  cshwshashlem1  17212  01eq0ringOLD  20721  ioombl1  25822  2irrexpq  27000  ppiublem1  27470  zabsle1  27564  gausslemma2dlem0f  27629  gausslemma2dlem0i  27632  gausslemma2dlem4  27637  2lgsoddprm  27684  ostth  27907  ltsval2  27924  ltsintdifex  27929  ltsres  27930  ltssolem1  27943  nosepnelem  27947  nb3grprlem1  29872  pthdivtx  30223  frgr3vlem1  30785  frgr3vlem2  30786  frgrwopreg  30835  frgrregorufr  30837  frgrregord13  30908  kur14lem7  35874  3jaodd  36377  dfrdg2  36455  dfrdg4  36613  iooelexlt  38181  relowlssretop  38182  wl-exeq  38362  iccpartiltu  48387  iccpartigtl  48388  icceuelpart  48401  prproropf1olem4  48471  fmtno4prmfac193  48541  fmtnofz04prm  48545  mogoldbblem  48701  grtriproplem  48920  grtrif1o  48923  gpgprismgr4cycllem7  49082  pgnbgreunbgrlem1  49094  pgnbgreunbgrlem2lem1  49095  pgnbgreunbgrlem2lem2  49096  pgnbgreunbgrlem2lem3  49097  pgnbgreunbgrlem2  49098  pgnbgreunbgrlem4  49100  pgnbgreunbgrlem5  49104  exple2lt6  49359