Theorem 3jaoi 1430

Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.)

Hypotheses

Ref	Expression
3jaoi.1	⊢ (𝜑 → 𝜓)
3jaoi.2	⊢ (𝜒 → 𝜓)
3jaoi.3	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
3jaoi	⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Proof of Theorem 3jaoi

Step	Hyp	Ref	Expression
1		3jaoi.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3		3jaoi.3	. . 3 ⊢ (𝜃 → 𝜓)
4	1, 2, 3	3pm3.2i 1340	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1427	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∨ w3o 1085   ∧ w3a 1086

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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaoian  1432  tpres  7175  ordzsl  7821  onzsl  7822  tfrlem16  8361  oawordeulem  8518  fsetexb  8837  elfiun  9381  infsupprpr  9457  domtriomlem  10395  axdc3lem2  10404  rankcf  10730  znegcl  12568  xrltnr  13079  xnegcl  13173  xnegneg  13174  xltnegi  13176  xnegid  13198  xaddrid  13201  xmulrid  13239  xrsupsslem  13267  xrinfmsslem  13268  reltxrnmnf  13303  elfznelfzo  13733  addmodlteq  13911  hashle2pr  14442  hashge2el2difr  14446  hashtpg  14450  hash1to3  14457  hash3tpde  14458  swrdnd0  14622  prm23lt5  16785  prm23ge5  16786  cshwshashlem1  17066  01eq0ringOLD  20440  ioombl1  25463  2irrexpq  26640  ppiublem1  27113  zabsle1  27207  gausslemma2dlem0f  27272  gausslemma2dlem0i  27275  gausslemma2dlem4  27280  2lgsoddprm  27327  ostth  27550  sltval2  27568  sltintdifex  27573  sltres  27574  sltsolem1  27587  nosepnelem  27591  nb3grprlem1  29307  pthdivtx  29657  frgr3vlem1  30202  frgr3vlem2  30203  frgrwopreg  30252  frgrregorufr  30254  frgrregord13  30325  kur14lem7  35199  3jaodd  35702  dfrdg2  35783  dfrdg4  35939  iooelexlt  37350  relowlssretop  37351  wl-exeq  37522  iccpartiltu  47420  iccpartigtl  47421  icceuelpart  47434  prproropf1olem4  47504  fmtno4prmfac193  47571  fmtnofz04prm  47575  mogoldbblem  47718  grtriproplem  47935  grtrif1o  47938  gpgprismgr4cycllem7  48088  pgnbgreunbgrlem1  48100  pgnbgreunbgrlem2lem1  48101  pgnbgreunbgrlem2lem2  48102  pgnbgreunbgrlem2lem3  48103  pgnbgreunbgrlem2  48104  pgnbgreunbgrlem4  48106  pgnbgreunbgrlem5  48110  exple2lt6  48349