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 401  df-or 861  df-3or 1104  df-3an 1105

This theorem is used by:  3jaoian  1457  tpres  7199  ordzsl  7837  onzsl  7838  tfrlem16  8376  oawordeulem  8535  fsetexb  8857  elfiun  9386  infsupprpr  9462  domtriomlem  10430  axdc3lem2  10439  rankcf  10766  znegcl  12633  xrltnr  13148  xnegcl  13243  xnegneg  13244  xltnegi  13246  xnegid  13268  xaddrid  13271  xmulrid  13309  xrsupsslem  13337  xrinfmsslem  13338  reltxrnmnf  13373  elfznelfzo  13807  addmodlteq  13987  hashle2pr  14519  hashge2el2difr  14523  hashtpg  14527  hash1to3  14534  hash3tpde  14535  swrdnd0  14700  prm23lt5  16878  prm23ge5  16879  cshwshashlem1  17159  01eq0ringOLD  20638  ioombl1  25730  2irrexpq  26905  ppiublem1  27375  zabsle1  27469  gausslemma2dlem0f  27534  gausslemma2dlem0i  27537  gausslemma2dlem4  27542  2lgsoddprm  27589  ostth  27812  ltsval2  27829  ltsintdifex  27834  ltsres  27835  ltssolem1  27848  nosepnelem  27852  nb3grprlem1  29739  pthdivtx  30085  frgr3vlem1  30633  frgr3vlem2  30634  frgrwopreg  30683  frgrregorufr  30685  frgrregord13  30756  kur14lem7  35712  3jaodd  36215  dfrdg2  36293  dfrdg4  36451  iooelexlt  38036  relowlssretop  38037  wl-exeq  38217  iccpartiltu  48199  iccpartigtl  48200  icceuelpart  48213  prproropf1olem4  48283  fmtno4prmfac193  48353  fmtnofz04prm  48357  mogoldbblem  48513  grtriproplem  48732  grtrif1o  48735  gpgprismgr4cycllem7  48894  pgnbgreunbgrlem1  48906  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  pgnbgreunbgrlem2  48910  pgnbgreunbgrlem4  48912  pgnbgreunbgrlem5  48916  exple2lt6  49172