Theorem 3jaoi 1455

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 1454	. 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  1458  tpres  7227  ordzsl  7877  onzsl  7878  tfrlem16  8426  oawordeulem  8587  fsetexb  8911  elfiun  9446  infsupprpr  9522  domtriomlem  10544  axdc3lem2  10553  rankcf  10886  znegcl  12755  xrltnr  13272  xnegcl  13367  xnegneg  13368  xltnegi  13370  xnegid  13392  xaddrid  13395  xmulrid  13433  xrsupsslem  13461  xrinfmsslem  13462  reltxrnmnf  13497  elfznelfzo  13932  addmodlteq  14113  hashle2pr  14646  hashge2el2difr  14650  hashtpg  14654  hash1to3  14661  hash3tpde  14662  swrdnd0  14832  prm23lt5  17018  prm23ge5  17019  cshwshashlem1  17299  01eq0ringOLD  20809  ioombl1  25910  2irrexpq  27086  ppiublem1  27556  zabsle1  27650  gausslemma2dlem0f  27715  gausslemma2dlem0i  27718  gausslemma2dlem4  27723  2lgsoddprm  27770  ostth  27993  ltsval2  28040  ltsintdifex  28045  ltsres  28046  ltssolem1  28059  nosepnelem  28063  nb3grprlem1  29988  pthdivtx  30339  frgr3vlem1  30901  frgr3vlem2  30902  frgrwopreg  30951  frgrregorufr  30953  frgrregord13  31024  kur14lem7  36143  3jaodd  36657  dfrdg2  36734  dfrdg4  36892  iooelexlt  38476  relowlssretop  38477  wl-exeq  38657  iccpartiltu  48707  iccpartigtl  48708  icceuelpart  48721  prproropf1olem4  48791  fmtno4prmfac193  48861  fmtnofz04prm  48865  mogoldbblem  49021  grtriproplem  49240  grtrif1o  49243  gpgprismgr4cycllem7  49402  pgnbgreunbgrlem1  49414  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  pgnbgreunbgrlem2lem3  49417  pgnbgreunbgrlem2  49418  pgnbgreunbgrlem4  49420  pgnbgreunbgrlem5  49424  exple2lt6  49679