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  7145  ordzsl  7785  onzsl  7786  tfrlem16  8322  oawordeulem  8479  fsetexb  8799  elfiun  9331  infsupprpr  9407  domtriomlem  10350  axdc3lem2  10359  rankcf  10686  znegcl  12524  xrltnr  13031  xnegcl  13126  xnegneg  13127  xltnegi  13129  xnegid  13151  xaddrid  13154  xmulrid  13192  xrsupsslem  13220  xrinfmsslem  13221  reltxrnmnf  13256  elfznelfzo  13687  addmodlteq  13867  hashle2pr  14398  hashge2el2difr  14402  hashtpg  14406  hash1to3  14413  hash3tpde  14414  swrdnd0  14579  prm23lt5  16740  prm23ge5  16741  cshwshashlem1  17021  01eq0ringOLD  20462  ioombl1  25517  2irrexpq  26694  ppiublem1  27167  zabsle1  27261  gausslemma2dlem0f  27326  gausslemma2dlem0i  27329  gausslemma2dlem4  27334  2lgsoddprm  27381  ostth  27604  sltval2  27622  sltintdifex  27627  sltres  27628  sltsolem1  27641  nosepnelem  27645  nb3grprlem1  29402  pthdivtx  29749  frgr3vlem1  30297  frgr3vlem2  30298  frgrwopreg  30347  frgrregorufr  30349  frgrregord13  30420  kur14lem7  35355  3jaodd  35858  dfrdg2  35936  dfrdg4  36094  iooelexlt  37506  relowlssretop  37507  wl-exeq  37678  iccpartiltu  47610  iccpartigtl  47611  icceuelpart  47624  prproropf1olem4  47694  fmtno4prmfac193  47761  fmtnofz04prm  47765  mogoldbblem  47908  grtriproplem  48127  grtrif1o  48130  gpgprismgr4cycllem7  48289  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  pgnbgreunbgrlem2  48305  pgnbgreunbgrlem4  48307  pgnbgreunbgrlem5  48311  exple2lt6  48552