Theorem 3jaoi 1449

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 1447	. 2 ⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
5	1, 2, 3, 4	mpbir3an 1356	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∨ w3o 1098

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 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101

This theorem is referenced by:  3jaoian  1452  tpres  7187  ordzsl  7827  onzsl  7828  tfrlem16  8366  oawordeulem  8525  fsetexb  8847  elfiun  9378  infsupprpr  9454  domtriomlem  10401  axdc3lem2  10410  rankcf  10737  znegcl  12608  xrltnr  13123  xnegcl  13218  xnegneg  13219  xltnegi  13221  xnegid  13243  xaddrid  13246  xmulrid  13284  xrsupsslem  13312  xrinfmsslem  13313  reltxrnmnf  13348  elfznelfzo  13781  addmodlteq  13961  hashle2pr  14492  hashge2el2difr  14496  hashtpg  14500  hash1to3  14507  hash3tpde  14508  swrdnd0  14673  prm23lt5  16852  prm23ge5  16853  cshwshashlem1  17133  01eq0ringOLD  20583  ioombl1  25626  2irrexpq  26798  ppiublem1  27268  zabsle1  27362  gausslemma2dlem0f  27427  gausslemma2dlem0i  27430  gausslemma2dlem4  27435  2lgsoddprm  27482  ostth  27705  ltsval2  27722  ltsintdifex  27727  ltsres  27728  ltssolem1  27741  nosepnelem  27745  nb3grprlem1  29583  pthdivtx  29929  frgr3vlem1  30477  frgr3vlem2  30478  frgrwopreg  30527  frgrregorufr  30529  frgrregord13  30600  kur14lem7  35567  3jaodd  36070  dfrdg2  36148  dfrdg4  36306  iooelexlt  37861  relowlssretop  37862  wl-exeq  38042  iccpartiltu  48033  iccpartigtl  48034  icceuelpart  48047  prproropf1olem4  48117  fmtno4prmfac193  48187  fmtnofz04prm  48191  mogoldbblem  48347  grtriproplem  48566  grtrif1o  48569  gpgprismgr4cycllem7  48728  pgnbgreunbgrlem1  48740  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  pgnbgreunbgrlem2lem3  48743  pgnbgreunbgrlem2  48744  pgnbgreunbgrlem4  48746  pgnbgreunbgrlem5  48750  exple2lt6  48991