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  7844  onzsl  7845  tfrlem16  8385  oawordeulem  8544  fsetexb  8868  elfiun  9403  infsupprpr  9479  domtriomlem  10447  axdc3lem2  10456  rankcf  10787  znegcl  12654  xrltnr  13170  xnegcl  13265  xnegneg  13266  xltnegi  13268  xnegid  13290  xaddrid  13293  xmulrid  13331  xrsupsslem  13359  xrinfmsslem  13360  reltxrnmnf  13395  elfznelfzo  13829  addmodlteq  14010  hashle2pr  14542  hashge2el2difr  14546  hashtpg  14550  hash1to3  14557  hash3tpde  14558  swrdnd0  14727  prm23lt5  16908  prm23ge5  16909  cshwshashlem1  17189  01eq0ringOLD  20691  ioombl1  25789  2irrexpq  26964  ppiublem1  27434  zabsle1  27528  gausslemma2dlem0f  27593  gausslemma2dlem0i  27596  gausslemma2dlem4  27601  2lgsoddprm  27648  ostth  27871  ltsval2  27888  ltsintdifex  27893  ltsres  27894  ltssolem1  27907  nosepnelem  27911  nb3grprlem1  29824  pthdivtx  30175  frgr3vlem1  30737  frgr3vlem2  30738  frgrwopreg  30787  frgrregorufr  30789  frgrregord13  30860  kur14lem7  35776  3jaodd  36279  dfrdg2  36357  dfrdg4  36515  iooelexlt  38101  relowlssretop  38102  wl-exeq  38282  iccpartiltu  48307  iccpartigtl  48308  icceuelpart  48321  prproropf1olem4  48391  fmtno4prmfac193  48461  fmtnofz04prm  48465  mogoldbblem  48621  grtriproplem  48840  grtrif1o  48843  gpgprismgr4cycllem7  49002  pgnbgreunbgrlem1  49014  pgnbgreunbgrlem2lem1  49015  pgnbgreunbgrlem2lem2  49016  pgnbgreunbgrlem2lem3  49017  pgnbgreunbgrlem2  49018  pgnbgreunbgrlem4  49020  pgnbgreunbgrlem5  49024  exple2lt6  49279