Theorem 3jaoi 1431

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 1341	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1428	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

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

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 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaoian  1433  tpres  7159  ordzsl  7799  onzsl  7800  tfrlem16  8336  oawordeulem  8493  fsetexb  8815  elfiun  9347  infsupprpr  9423  domtriomlem  10366  axdc3lem2  10375  rankcf  10702  znegcl  12540  xrltnr  13047  xnegcl  13142  xnegneg  13143  xltnegi  13145  xnegid  13167  xaddrid  13170  xmulrid  13208  xrsupsslem  13236  xrinfmsslem  13237  reltxrnmnf  13272  elfznelfzo  13703  addmodlteq  13883  hashle2pr  14414  hashge2el2difr  14418  hashtpg  14422  hash1to3  14429  hash3tpde  14430  swrdnd0  14595  prm23lt5  16756  prm23ge5  16757  cshwshashlem1  17037  01eq0ringOLD  20481  ioombl1  25536  2irrexpq  26713  ppiublem1  27186  zabsle1  27280  gausslemma2dlem0f  27345  gausslemma2dlem0i  27348  gausslemma2dlem4  27353  2lgsoddprm  27400  ostth  27623  ltsval2  27641  ltsintdifex  27646  ltsres  27647  ltssolem1  27660  nosepnelem  27664  nb3grprlem1  29471  pthdivtx  29818  frgr3vlem1  30366  frgr3vlem2  30367  frgrwopreg  30416  frgrregorufr  30418  frgrregord13  30489  kur14lem7  35434  3jaodd  35937  dfrdg2  36015  dfrdg4  36173  iooelexlt  37644  relowlssretop  37645  wl-exeq  37818  iccpartiltu  47811  iccpartigtl  47812  icceuelpart  47825  prproropf1olem4  47895  fmtno4prmfac193  47962  fmtnofz04prm  47966  mogoldbblem  48109  grtriproplem  48328  grtrif1o  48331  gpgprismgr4cycllem7  48490  pgnbgreunbgrlem1  48502  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  pgnbgreunbgrlem2lem3  48505  pgnbgreunbgrlem2  48506  pgnbgreunbgrlem4  48508  pgnbgreunbgrlem5  48512  exple2lt6  48753