MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Unicode version

Theorem mpi 17
Description: A nested modus ponens inference. Inference associated with com12 31. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypotheses
Ref Expression
mpi.1
mpi.2
Assertion
Ref Expression
mpi

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3
21a1i 11 . 2
3 mpi.2 . 2
42, 3mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  mpisyl  18  mp2OLD  19  syl6mpi  62  mp2ani  678  mp3an3  1313  merco2  1569  equs4v  1787  equcomi  1793  equviniv  1803  19.8aOLD  1858  aev  1943  spimt  2005  equs4  2035  ax12v2  2083  2ax6elem  2193  ax12eq  2271  ax12el  2272  ax12inda  2278  ax12v2-o  2279  pm13.183  3240  sbcth  3342  sbcth2  3422  ssun3  3668  ssun4  3669  uneqdifeq  3916  ralf0  3936  uniintsn  4324  rext  4700  exss  4715  uniopel  4756  wefrc  4878  ordun  4984  relop  5158  dmrnssfld  5266  iss  5326  sofld  5460  relcoi1  5541  nfunv  5624  funimass2  5667  fvbr0  5892  fvmptg  5954  fovcl  6407  ov3  6439  elovmpt2  6520  limsssuc  6685  tfisi  6693  finds1  6729  frxp  6910  tfrlem1  7064  oaordi  7214  oaword2  7221  omeulem1  7250  oeworde  7261  oelim2  7263  nnaordi  7286  oaabs2  7313  0domg  7664  limenpsi  7712  enp1i  7775  findcard2  7780  ordunifi  7790  fidomdm  7822  dffi3  7911  oismo  7986  wdom2d  8027  wdomima2g  8033  suc11reg  8057  elom3  8086  cantnfval2  8109  cantnfval2OLD  8139  rankunb  8289  rankval4  8306  karden  8334  cardsn  8371  cardlim  8374  cardprclem  8381  fseqdom  8428  dfac12lem3  8546  kmlem2  8552  kmlem10  8560  cflim2  8664  cfslb2n  8669  fin23lem27  8729  axcc3  8839  axcc4  8840  acncc  8841  domtriomlem  8843  axdclem2  8921  imadomg  8933  alephval2  8968  alephreg  8978  axextnd  8987  fpwwe2lem10  9038  pwfseq  9063  gch2  9074  axgroth3  9230  inaprc  9235  nlt1pi  9305  indpi  9306  1re  9616  mul02lem2  9778  addid1  9781  fimaxre  10515  supmul1  10533  inelr  10551  rimul  10552  nnge1  10587  zneo  10970  uzindOLD  10982  ltweuz  12072  hashrabsn1  12442  hashf1lem2  12505  hash2pwpr  12519  climuni  13375  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  fprod2d  13785  efne0  13832  ruclem13  13975  dvdslelem  14030  divalglem0  14051  prmreclem2  14435  prmreclem3  14436  mreexexd  15045  coaval  15395  xpcco  15452  pltirr  15593  frgpnabllem1  16877  ablfac1eulem  17123  mdetunilem9  19122  mretopd  19593  fiuncmp  19904  ptcmpfi  20314  filtop  20356  supnfcls  20521  flimfnfcls  20529  alexsubALTlem2  20548  alexsubALTlem4  20550  trust  20732  rectbntr0  21337  fsumcn  21374  ovoliunlem3  21915  ovolicc2lem4  21931  dyadmax  22007  vitali  22022  itgfsum  22233  dvmptfsum  22376  fta1g  22568  fta1  22704  aannenlem1  22724  aalioulem3  22730  logltb  22984  logdmn0  23021  ang180lem2  23142  angpined  23161  mumullem2  23454  dchrisum0re  23698  chpdifbnd  23740  pntrlog2bnd  23769  pntibndlem3  23777  pnt3  23797  nbgraop  24423  isuvtx  24488  0eusgraiff0rgra  24939  frgrancvvdeqlem4  25033  dvrunz  25435  hiidge0  26015  chsupval  26253  chsupcl  26258  chsupss  26260  ococin  26326  chsupval2  26328  ssjo  26365  h1de2i  26471  pjss2i  26598  pjssmii  26599  sto2i  27156  stge1i  27157  stle0i  27158  stlei  27159  stlesi  27160  stm1i  27162  staddi  27165  stadd3i  27167  golem1  27190  stcltrlem1  27195  mdexchi  27254  chirred  27314  atabsi  27320  rmoeq  27386  abrexdomjm  27405  ifbieq12d2  27420  iocinif  27592  voliune  28201  volfiniune  28202  probdif  28359  kur14lem9  28658  relexp1  29054  wfrlem5  29347  wfrlem16  29358  frrlem5  29391  nofv  29417  noprc  29441  sscoid  29563  limsucncmpi  29910  wl-embantALT  29975  supaddc  30041  abrexdom  30221  heiborlem10  30316  pellexlem3  30767  pell1234qrne0  30789  hbtlem6  31078  radcnvrat  31195  fzisoeu  31500  funressnfv  32213  faovcl  32285  cznnring  32764  zlmodzxznm  33098  3impexpbicom  33221  sb5ALT  33295  eexinst01  33296  ax6e2eq  33330  sineq0ALT  33737  bnj849  33983  bj-alequex  34268  bj-spimtv  34278  bj-axc15v  34330  bj-exlimmpi  34477  cvrnrefN  35007  pmod1i  35572  pmodN  35574  osumcllem11N  35690  pexmidlem8N  35701  pl42lem3N  35705  cdleme18b  36017  dochexmidlem8  37194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator