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. (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  1304  merco2  1544  equcomi  1733  equviniv  1743  19.8a  1797  19.8aOLD  1798  aev  1881  spimt  1961  equs4  1995  ax12v2  2043  2ax6elem  2166  ax12eq  2251  ax12el  2252  ax12inda  2258  ax12v2-o  2259  pm13.183  3210  sbcth  3312  sbcth2  3392  ssun3  3635  ssun4  3636  uneqdifeq  3881  ralf0  3900  uniintsn  4282  rext  4657  exss  4672  uniopel  4712  wefrc  4831  ordun  4937  relop  5107  dmrnssfld  5215  iss  5272  sofld  5405  relcoi1  5485  nfunv  5568  funimass2  5611  fvbr0  5834  fvmptg  5895  fovcl  6328  ov3  6360  elovmpt2  6440  limsssuc  6594  tfisi  6602  finds1  6638  frxp  6816  tfrlem1  6969  oaordi  7119  oaword2  7126  omeulem1  7155  oeworde  7166  oelim2  7168  nnaordi  7191  oaabs2  7218  0domg  7572  limenpsi  7620  enp1i  7682  findcard2  7687  ordunifi  7697  fidomdm  7728  dffi3  7817  oismo  7891  wdom2d  7932  wdomima2g  7938  suc11reg  7962  elom3  7991  cantnfval2  8014  cantnfval2OLD  8044  rankunb  8194  rankval4  8211  karden  8239  cardsn  8276  cardlim  8279  cardprclem  8286  fseqdom  8333  dfac12lem3  8451  kmlem2  8457  kmlem10  8465  cflim2  8569  cfslb2n  8574  fin23lem27  8634  axcc3  8744  axcc4  8745  acncc  8746  domtriomlem  8748  axdclem2  8826  imadomg  8838  alephval2  8873  alephreg  8883  axextnd  8892  fpwwe2lem10  8943  pwfseq  8968  gch2  8979  axgroth3  9135  inaprc  9140  nlt1pi  9212  indpi  9213  1re  9522  mul02lem2  9683  addid1  9686  fimaxre  10414  supmul1  10432  inelr  10450  rimul  10451  nnge1  10486  zneo  10862  uzindOLD  10874  ltweuz  11929  hash2pwpr  12340  hashf1lem2  12367  climuni  13188  fsum2d  13396  fsumabs  13422  fsumrlim  13432  fsumo1  13433  fsumiun  13442  efne0  13539  ruclem13  13682  dvdslelem  13735  divalglem0  13755  prmreclem2  14136  prmreclem3  14137  mreexexd  14745  coaval  15095  xpcco  15152  pltirr  15292  frgpnabllem1  16512  ablfac1eulem  16748  mdetunilem9  18694  mretopd  19095  fiuncmp  19406  ptcmpfi  19785  filtop  19827  supnfcls  19992  flimfnfcls  20000  alexsubALTlem2  20019  alexsubALTlem4  20021  trust  20203  rectbntr0  20808  fsumcn  20845  ovoliunlem3  21386  ovolicc2lem4  21402  dyadmax  21478  vitali  21493  itgfsum  21704  dvmptfsum  21847  fta1g  22039  fta1  22174  aannenlem1  22194  aalioulem3  22200  logltb  22448  logdmn0  22485  ang180lem2  22606  angpined  22625  mumullem2  22918  dchrisum0re  23162  chpdifbnd  23204  pntrlog2bnd  23233  pntibndlem3  23241  pnt3  23261  nbgraop  23804  isuvtx  23865  dvrunz  24389  hiidge0  24969  chsupval  25207  chsupcl  25212  chsupss  25214  ococin  25280  chsupval2  25282  ssjo  25319  h1de2i  25425  pjss2i  25552  pjssmii  25553  sto2i  26110  stge1i  26111  stle0i  26112  stlei  26113  stlesi  26114  stm1i  26116  staddi  26119  stadd3i  26121  golem1  26144  stcltrlem1  26149  mdexchi  26208  chirred  26268  atabsi  26274  rmoeq  26340  abrexdomjm  26357  ifbieq12d2  26372  iocinif  26532  voliune  27101  volfiniune  27102  sibfof  27182  probdif  27259  kur14lem9  27558  relexp1  27789  fprod2d  27948  wfrlem5  28184  wfrlem16  28195  frrlem5  28228  nofv  28254  noprc  28278  sscoid  28400  limsucncmpi  28747  wl-embantALT  28812  supaddc  28877  abrexdom  29084  heiborlem10  29179  pellexlem3  29632  pell1234qrne0  29654  hbtlem6  29945  funressnfv  30911  faovcl  30983  hashrabsn1  31110  0eusgraiff0rgra  31429  frgrancvvdeqlem4  31503  zlmodzxznm  31811  3impexpbicom  31999  sb5ALT  32073  eexinst01  32074  ax6e2eq  32109  sineq0ALT  32516  bnj849  32761  bj-alequex  33049  bj-spimtv  33059  bj-equs4v  33090  bj-axc15v  33110  bj-exlimmpi  33257  cvrnrefN  33778  pmod1i  34343  pmodN  34345  osumcllem11N  34461  pexmidlem8N  34472  pl42lem3N  34476  cdleme18b  34787  dochexmidlem8  35963  frege58b  36581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator