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  7207  ordzsl  7856  onzsl  7857  tfrlem16  8401  oawordeulem  8562  fsetexb  8886  elfiun  9422  infsupprpr  9498  domtriomlem  10520  axdc3lem2  10529  rankcf  10862  znegcl  12731  xrltnr  13248  xnegcl  13343  xnegneg  13344  xltnegi  13346  xnegid  13368  xaddrid  13371  xmulrid  13409  xrsupsslem  13437  xrinfmsslem  13438  reltxrnmnf  13473  elfznelfzo  13908  addmodlteq  14089  hashle2pr  14622  hashge2el2difr  14626  hashtpg  14630  hash1to3  14637  hash3tpde  14638  swrdnd0  14807  prm23lt5  16992  prm23ge5  16993  cshwshashlem1  17273  01eq0ringOLD  20782  ioombl1  25883  2irrexpq  27059  ppiublem1  27529  zabsle1  27623  gausslemma2dlem0f  27688  gausslemma2dlem0i  27691  gausslemma2dlem4  27696  2lgsoddprm  27743  ostth  27966  ltsval2  28013  ltsintdifex  28018  ltsres  28019  ltssolem1  28032  nosepnelem  28036  nb3grprlem1  29961  pthdivtx  30312  frgr3vlem1  30874  frgr3vlem2  30875  frgrwopreg  30924  frgrregorufr  30926  frgrregord13  30997  kur14lem7  35977  3jaodd  36480  dfrdg2  36557  dfrdg4  36715  iooelexlt  38286  relowlssretop  38287  wl-exeq  38467  iccpartiltu  48504  iccpartigtl  48505  icceuelpart  48518  prproropf1olem4  48588  fmtno4prmfac193  48658  fmtnofz04prm  48662  mogoldbblem  48818  grtriproplem  49037  grtrif1o  49040  gpgprismgr4cycllem7  49199  pgnbgreunbgrlem1  49211  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  pgnbgreunbgrlem2lem3  49214  pgnbgreunbgrlem2  49215  pgnbgreunbgrlem4  49217  pgnbgreunbgrlem5  49221  exple2lt6  49476