MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jaoi Structured version   Visualization version   GIF version

Theorem 3jaoi 1539
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
StepHypRef Expression
1 3jaoi.1 . . 3 (𝜑𝜓)
2 3jaoi.2 . . 3 (𝜒𝜓)
3 3jaoi.3 . . 3 (𝜃𝜓)
41, 2, 33pm3.2i 1423 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1536 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1070  w3a 1071
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 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073
This theorem is referenced by:  3jaoian  1541  tpres  6610  ordzsl  7192  onzsl  7193  tfrlem16  7642  oawordeulem  7788  elfiun  8492  domtriomlem  9466  axdc3lem2  9475  rankcf  9801  znegcl  11614  xrltnr  12158  xnegcl  12249  xnegneg  12250  xltnegi  12252  xnegid  12274  xaddid1  12277  xmulid1  12314  xrsupsslem  12342  xrinfmsslem  12343  reltxrnmnf  12377  elfznelfzo  12781  addmodlteq  12953  hashle2pr  13461  hashge2el2difr  13465  hashtpg  13469  hash1to3  13475  prm23lt5  15726  prm23ge5  15727  cshwshashlem1  16009  01eq0ring  19487  ioombl1  23550  ppiublem1  25148  zabsle1  25242  gausslemma2dlem0f  25307  gausslemma2dlem0i  25310  gausslemma2dlem4  25315  2lgsoddprm  25362  ostth  25549  nb3grprlem1  26505  pthdivtx  26860  frgr3vlem1  27455  frgr3vlem2  27456  frgrwopreg  27505  frgrregorufr  27507  frgrregord13  27595  kur14lem7  31532  3jaodd  31933  dfrdg2  32037  sltval2  32146  sltintdifex  32151  sltres  32152  sltsolem1  32163  nosepnelem  32167  dfrdg4  32395  iooelexlt  33547  relowlssretop  33548  wl-exeq  33656  iccpartiltu  41886  iccpartigtl  41887  icceuelpart  41900  fmtno4prmfac193  42013  fmtnofz04prm  42017  mogoldbblem  42157  exple2lt6  42673
  Copyright terms: Public domain W3C validator