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, 5-Aug-1993.) (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:  mp2ALT  18  syl6mpi  61  mp2ani  663  mp3an3  1288  3impexpbicom  1403  ee10  1411  merco2  1537  equcomi  1724  equviniv  1734  19.8a  1786  spimt  1940  equs4  1974  ax12v2  2024  2sb6rflem1  2149  ax12eq  2233  ax12el  2234  ax12inda  2240  ax12v2-o  2241  pm13.183  3078  sbcth  3178  sbcth2  3258  ssun3  3498  ssun4  3499  uneqdifeq  3744  ralf0  3763  uniintsn  4140  rext  4512  exss  4527  uniopel  4567  wefrc  4685  ordun  4791  relop  4961  dmrnssfld  5069  iss  5126  sofld  5258  relcoi1  5338  nfunv  5421  funimass2  5462  fvbr0  5681  fvmptg  5742  fovcl  6165  ov3  6197  elovmpt2  6277  limsssuc  6431  tfisi  6439  finds1  6475  frxp  6651  tfrlem1  6794  oaordi  6946  oaword2  6953  omeulem1  6982  oeworde  6993  oelim2  6995  nnaordi  7018  oaabs2  7045  0domg  7397  limenpsi  7445  enp1i  7506  findcard2  7511  ordunifi  7521  fidomdm  7552  dffi3  7628  oismo  7701  wdom2d  7742  wdomima2g  7748  suc11reg  7772  elom3  7801  cantnfval2  7824  cantnfval2OLD  7854  rankunb  8004  rankval4  8021  karden  8049  cardsn  8086  cardlim  8089  cardprclem  8096  fseqdom  8143  dfac12lem3  8261  kmlem2  8267  kmlem10  8275  cflim2  8379  cfslb2n  8384  fin23lem27  8444  axcc3  8554  axcc4  8555  acncc  8556  domtriomlem  8558  axdclem2  8636  imadomg  8648  alephval2  8683  alephreg  8693  axextnd  8702  fpwwe2lem10  8752  pwfseq  8777  gch2  8788  axgroth3  8944  inaprc  8949  nlt1pi  9021  indpi  9022  1re  9331  mul02lem2  9492  addid1  9495  fimaxre  10223  supmul1  10241  inelr  10258  rimul  10259  nnge1  10294  zneo  10669  uzindOLD  10681  ltweuz  11725  hash2pwpr  12123  hashf1lem2  12150  climuni  12971  fsum2d  13179  fsumabs  13204  fsumrlim  13214  fsumo1  13215  fsumiun  13224  efne0  13321  ruclem13  13464  dvdslelem  13517  divalglem0  13537  prmreclem2  13918  prmreclem3  13919  mreexexd  14526  coaval  14876  xpcco  14933  pltirr  15073  frgpnabllem1  16287  ablfac1eulem  16439  mdetunilem9  18128  mretopd  18400  fiuncmp  18711  ptcmpfi  19090  filtop  19132  supnfcls  19297  flimfnfcls  19305  alexsubALTlem2  19324  alexsubALTlem4  19326  trust  19504  rectbntr0  20109  fsumcn  20146  ovoliunlem3  20687  ovolicc2lem4  20703  dyadmax  20778  vitali  20793  itgfsum  21004  dvmptfsum  21147  fta1g  21380  fta1  21515  aannenlem1  21535  aalioulem3  21541  logltb  21789  logdmn0  21826  ang180lem2  21947  angpined  21966  mumullem2  22259  dchrisum0re  22503  chpdifbnd  22545  pntrlog2bnd  22574  pntibndlem3  22582  pnt3  22602  nbgraop  23014  isuvtx  23075  dvrunz  23599  hiidge0  24179  chsupval  24417  chsupcl  24422  chsupss  24424  ococin  24490  chsupval2  24492  ssjo  24529  h1de2i  24635  pjss2i  24762  pjssmii  24763  sto2i  25320  stge1i  25321  stle0i  25322  stlei  25323  stlesi  25324  stm1i  25326  staddi  25329  stadd3i  25331  golem1  25354  stcltrlem1  25359  mdexchi  25418  chirred  25478  atabsi  25484  rmoeq  25551  abrexdomjm  25568  ifbieq12d2  25583  iocinif  25749  voliune  26354  volfiniune  26355  sibfof  26429  probdif  26506  kur14lem9  26805  relexp1  27035  fprod2d  27194  wfrlem5  27430  wfrlem16  27441  frrlem5  27474  nofv  27500  noprc  27524  sscoid  27646  limsucncmpi  27994  wl-embantALT  28054  wl-equsal1t  28063  wl-ax12v2  28081  supaddc  28088  abrexdom  28295  heiborlem10  28390  pellexlem3  28845  pell1234qrne0  28867  hbtlem6  29158  funressnfv  29708  faovcl  29780  hashrabsn1  29907  0eusgraiff0rgra  30226  frgrancvvdeqlem4  30300  zlmodzxznm  30623  sb5ALT  30807  eexinst01  30808  ax6e2eq  30843  sineq0ALT  31251  bnj849  31496  bj-alequex  31710  bj-spimtv  31720  bj-equs4v  31751  bj-axc15v  31771  bj-vtoclgf  31870  cvrnrefN  32364  pmod1i  32929  pmodN  32931  osumcllem11N  33047  pexmidlem8N  33058  pl42lem3N  33062  cdleme18b  33373  dochexmidlem8  34549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator