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

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

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 mpi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpisyl  21  syl6mpi  64  mp2ani  689  mp3an3  1362  merco2  1629  equs4v  1856  equcomiv  1868  equcomi  1871  equviniv  1882  aev  2036  spimt  2107  equs4  2137  ax12v2  2185  2ax6elem  2288  pm13.183  3190  sbcth  3293  sbcth2  3362  ssun3  3610  ssun4  3611  uneqdifeq  3867  ralf0  3887  elpreqprlem  4173  uniintsn  4285  rext  4661  exss  4676  uniopel  4718  wefrc  4846  relop  5003  dmrnssfld  5111  iss  5170  sofld  5302  relcoi1OLD  5383  ordun  5542  nfunv  5631  funimass2  5678  fvbr0  5908  fvmptg  5968  fovcl  6427  ov3  6459  elovmpt2  6540  limsssuc  6703  tfisi  6711  finds1  6748  frxp  6932  wfrlem5  7065  wfrlem16  7076  dfrecs3  7116  tfrlem1  7119  oaordi  7272  oaword2  7279  omeulem1  7308  oeworde  7319  oelim2  7321  nnaordi  7344  oaabs2  7371  0domg  7724  limenpsi  7772  enp1i  7831  findcard2  7836  ordunifi  7846  fidomdm  7878  dffi3  7970  oismo  8080  wdom2d  8120  wdomima2g  8126  suc11reg  8149  elom3  8178  cantnfval2  8199  rankunb  8346  rankval4  8363  karden  8391  cardsn  8428  cardlim  8431  cardprclem  8438  fseqdom  8482  dfac12lem3  8600  kmlem2  8606  kmlem10  8614  cflim2  8718  cfslb2n  8723  fin23lem27  8783  axcc3  8893  axcc4  8894  acncc  8895  domtriomlem  8897  axdclem2  8975  imadomg  8987  alephval2  9022  alephreg  9032  axextnd  9041  fpwwe2lem10  9089  pwfseq  9114  gch2  9125  axgroth3  9281  inaprc  9286  nlt1pi  9356  indpi  9357  1re  9667  mul02lem2  9835  addid1  9838  fimaxre  10578  supaddc  10601  supmul1  10603  inelr  10626  rimul  10627  nnge1  10662  zneo  11046  ltweuz  12206  hashrabsn1  12584  hashf1lem2  12651  hash2pwpr  12667  climuni  13664  fsum2d  13880  fsumabs  13909  fsumrlim  13919  fsumo1  13920  fsumiun  13929  fprod2d  14083  efne0  14199  ruclem13  14342  dvdslelem  14397  divalglem0  14419  lcmfnnval  14642  lcmfnnvalOLD  14645  prmreclem2  14909  prmreclem3  14910  mreexexd  15602  coaval  16011  xpcco  16116  pltirr  16257  frgpnabllem1  17557  ablfac1eulem  17753  mdetunilem9  19693  mretopd  20156  fiuncmp  20467  ptcmpfi  20876  filtop  20918  supnfcls  21083  flimfnfcls  21091  alexsubALTlem2  21111  alexsubALTlem4  21113  trust  21292  rectbntr0  21898  fsumcn  21950  ovoliunlem3  22505  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  dyadmax  22604  vitali  22619  itgfsum  22832  dvmptfsum  22975  fta1g  23166  fta1  23309  aannenlem1  23332  aalioulem3  23338  logltb  23597  logdmn0  23633  ang180lem2  23787  angpined  23804  mumullem2  24155  dchrisum0re  24399  chpdifbnd  24441  pntrlog2bnd  24470  pntibndlem3  24478  pnt3  24498  nbgraop  25199  isuvtx  25264  0eusgraiff0rgra  25715  frgrancvvdeqlem4  25809  dvrunz  26209  hiidge0  26799  chsupval  27036  chsupcl  27041  chsupss  27043  ococin  27109  chsupval2  27111  ssjo  27148  h1de2i  27254  pjss2i  27381  pjssmii  27382  sto2i  27938  stge1i  27939  stle0i  27940  stlei  27941  stlesi  27942  stm1i  27944  staddi  27947  stadd3i  27949  golem1  27972  stcltrlem1  27977  mdexchi  28036  chirred  28096  atabsi  28102  rmoeqALT  28171  abrexdomjm  28189  ifbieq12d2  28207  iocinif  28411  voliune  29100  volfiniune  29101  probdif  29301  bnj849  29784  kur14lem9  29985  frrlem5  30566  nofv  30592  noprc  30618  sscoid  30728  limsucncmpi  31153  bj-sbex  31283  bj-alequex  31353  bj-spimtv  31363  bj-axc15v  31406  bj-exlimmpi  31556  finxpreclem4  31830  wl-embantALT  31891  wl-orel12  31893  wl-euequ1f  31947  wl-ax12v3  31956  poimirlem9  31993  abrexdom  32101  heiborlem10  32196  ax12eq  32556  ax12el  32557  ax12inda  32563  ax12v2-o  32564  cvrnrefN  32892  pmod1i  33457  pmodN  33459  osumcllem11N  33575  pexmidlem8N  33586  pl42lem3N  33590  cdleme18b  33902  dochexmidlem8  35079  pellexlem3  35719  pell1234qrne0  35743  hbtlem6  36032  radcnvrat  36706  3impexpbicom  36877  sb5ALT  36925  eexinst01  36926  ax6e2eq  36967  sineq0ALT  37373  fzisoeu  37555  ovnsubaddlem2  38430  funressnfv  38666  faovcl  38739  mod2eq1n2dvds  38762  propssopi  39039  funsndifnop  39063  nbgrval  39455  upgrewlkle2  39672  cznnring  40230  zlmodzxznm  40562  nn0o1gt2  40599  elbigolo1  40640  dignn0flhalflem1  40698  nn0sumshdig  40706
  Copyright terms: Public domain W3C validator