Theorem 3jaoi 1452

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

Syntax hints:   → wi 4   ∨ w3o 1100

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 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103

This theorem is referenced by:  3jaoian  1455  tpres  7200  ordzsl  7841  onzsl  7842  tfrlem16  8380  oawordeulem  8539  fsetexb  8861  elfiun  9390  infsupprpr  9466  domtriomlem  10426  axdc3lem2  10435  rankcf  10762  znegcl  12629  xrltnr  13144  xnegcl  13239  xnegneg  13240  xltnegi  13242  xnegid  13264  xaddrid  13267  xmulrid  13305  xrsupsslem  13333  xrinfmsslem  13334  reltxrnmnf  13369  elfznelfzo  13802  addmodlteq  13982  hashle2pr  14514  hashge2el2difr  14518  hashtpg  14522  hash1to3  14529  hash3tpde  14530  swrdnd0  14695  prm23lt5  16874  prm23ge5  16875  cshwshashlem1  17155  01eq0ringOLD  20615  ioombl1  25690  2irrexpq  26862  ppiublem1  27332  zabsle1  27426  gausslemma2dlem0f  27491  gausslemma2dlem0i  27494  gausslemma2dlem4  27499  2lgsoddprm  27546  ostth  27769  ltsval2  27786  ltsintdifex  27791  ltsres  27792  ltssolem1  27805  nosepnelem  27809  nb3grprlem1  29671  pthdivtx  30017  frgr3vlem1  30565  frgr3vlem2  30566  frgrwopreg  30615  frgrregorufr  30617  frgrregord13  30688  kur14lem7  35637  3jaodd  36140  dfrdg2  36218  dfrdg4  36376  iooelexlt  37930  relowlssretop  37931  wl-exeq  38111  iccpartiltu  48094  iccpartigtl  48095  icceuelpart  48108  prproropf1olem4  48178  fmtno4prmfac193  48248  fmtnofz04prm  48252  mogoldbblem  48408  grtriproplem  48627  grtrif1o  48630  gpgprismgr4cycllem7  48789  pgnbgreunbgrlem1  48801  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  pgnbgreunbgrlem2lem3  48804  pgnbgreunbgrlem2  48805  pgnbgreunbgrlem4  48807  pgnbgreunbgrlem5  48811  exple2lt6  49063