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

Theorem 3jaoi 1389
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 1237 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1387 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1035  w3a 1036
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-or 385  df-an 386  df-3or 1037  df-3an 1038
This theorem is referenced by:  3jaoian  1391  tpres  6451  ordzsl  7030  onzsl  7031  tfrlem16  7474  oawordeulem  7619  elfiun  8321  domtriomlem  9249  axdc3lem2  9258  rankcf  9584  znegcl  11397  xrltnr  11938  xnegcl  12029  xnegneg  12030  xltnegi  12032  xnegid  12054  xaddid1  12057  xmulid1  12094  xrsupsslem  12122  xrinfmsslem  12123  reltxrnmnf  12157  elfznelfzo  12557  addmodlteq  12728  hashle2pr  13242  hashge2el2difr  13246  hashtpg  13250  hash1to3  13256  prm23lt5  15500  prm23ge5  15501  cshwshashlem1  15783  01eq0ring  19253  ioombl1  23311  ppiublem1  24908  zabsle1  25002  gausslemma2dlem0f  25067  gausslemma2dlem0i  25070  gausslemma2dlem4  25075  2lgsoddprm  25122  ostth  25309  nb3grprlem1  26263  pthdivtx  26606  frgr3vlem1  27117  frgr3vlem2  27118  frgrwopreg  27159  frgrregorufr  27163  frgrregord13  27224  kur14lem7  31168  3jaodd  31570  dfrdg2  31675  sltval2  31783  sltintdifex  31788  sltres  31789  sltsolem1  31800  nosepnelem  31804  dfrdg4  32033  iooelexlt  33181  relowlssretop  33182  wl-exeq  33292  iccpartiltu  41122  iccpartigtl  41123  icceuelpart  41136  fmtno4prmfac193  41250  fmtnofz04prm  41254  mogoldbblem  41394  exple2lt6  41910
  Copyright terms: Public domain W3C validator