MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Structured version   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  |-  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  18  mp2OLD  19  syl6mpi  62  mp2ani  678  mp3an3  1312  merco2  1554  equs4v  1771  equcomi  1777  equviniv  1787  19.8aOLD  1842  aev  1927  spimt  1989  equs4  2019  ax12v2  2067  2ax6elem  2177  ax12eq  2255  ax12el  2256  ax12inda  2262  ax12v2-o  2263  pm13.183  3224  sbcth  3326  sbcth2  3406  ssun3  3651  ssun4  3652  uneqdifeq  3898  ralf0  3917  uniintsn  4305  rext  4681  exss  4696  uniopel  4737  wefrc  4859  ordun  4965  relop  5139  dmrnssfld  5247  iss  5307  sofld  5441  relcoi1  5522  nfunv  5605  funimass2  5648  fvbr0  5873  fvmptg  5935  fovcl  6388  ov3  6420  elovmpt2  6501  limsssuc  6666  tfisi  6674  finds1  6710  frxp  6891  tfrlem1  7043  oaordi  7193  oaword2  7200  omeulem1  7229  oeworde  7240  oelim2  7242  nnaordi  7265  oaabs2  7292  0domg  7642  limenpsi  7690  enp1i  7753  findcard2  7758  ordunifi  7768  fidomdm  7800  dffi3  7889  oismo  7963  wdom2d  8004  wdomima2g  8010  suc11reg  8034  elom3  8063  cantnfval2  8086  cantnfval2OLD  8116  rankunb  8266  rankval4  8283  karden  8311  cardsn  8348  cardlim  8351  cardprclem  8358  fseqdom  8405  dfac12lem3  8523  kmlem2  8529  kmlem10  8537  cflim2  8641  cfslb2n  8646  fin23lem27  8706  axcc3  8816  axcc4  8817  acncc  8818  domtriomlem  8820  axdclem2  8898  imadomg  8910  alephval2  8945  alephreg  8955  axextnd  8964  fpwwe2lem10  9015  pwfseq  9040  gch2  9051  axgroth3  9207  inaprc  9212  nlt1pi  9282  indpi  9283  1re  9593  mul02lem2  9755  addid1  9758  fimaxre  10491  supmul1  10509  inelr  10527  rimul  10528  nnge1  10563  zneo  10946  uzindOLD  10958  ltweuz  12046  hashrabsn1  12416  hashf1lem2  12479  hash2pwpr  12493  climuni  13349  fsum2d  13560  fsumabs  13589  fsumrlim  13599  fsumo1  13600  fsumiun  13609  efne0  13704  ruclem13  13847  dvdslelem  13902  divalglem0  13923  prmreclem2  14307  prmreclem3  14308  mreexexd  14917  coaval  15264  xpcco  15321  pltirr  15462  frgpnabllem1  16746  ablfac1eulem  16991  mdetunilem9  18989  mretopd  19459  fiuncmp  19770  ptcmpfi  20180  filtop  20222  supnfcls  20387  flimfnfcls  20395  alexsubALTlem2  20414  alexsubALTlem4  20416  trust  20598  rectbntr0  21203  fsumcn  21240  ovoliunlem3  21781  ovolicc2lem4  21797  dyadmax  21873  vitali  21888  itgfsum  22099  dvmptfsum  22242  fta1g  22434  fta1  22569  aannenlem1  22589  aalioulem3  22595  logltb  22849  logdmn0  22886  ang180lem2  23007  angpined  23026  mumullem2  23319  dchrisum0re  23563  chpdifbnd  23605  pntrlog2bnd  23634  pntibndlem3  23642  pnt3  23662  nbgraop  24288  isuvtx  24353  0eusgraiff0rgra  24804  frgrancvvdeqlem4  24898  dvrunz  25300  hiidge0  25880  chsupval  26118  chsupcl  26123  chsupss  26125  ococin  26191  chsupval2  26193  ssjo  26230  h1de2i  26336  pjss2i  26463  pjssmii  26464  sto2i  27021  stge1i  27022  stle0i  27023  stlei  27024  stlesi  27025  stm1i  27027  staddi  27030  stadd3i  27032  golem1  27055  stcltrlem1  27060  mdexchi  27119  chirred  27179  atabsi  27185  rmoeq  27251  abrexdomjm  27270  ifbieq12d2  27285  iocinif  27457  voliune  28067  volfiniune  28068  probdif  28225  kur14lem9  28524  relexp1  28920  fprod2d  29079  wfrlem5  29315  wfrlem16  29326  frrlem5  29359  nofv  29385  noprc  29409  sscoid  29531  limsucncmpi  29878  wl-embantALT  29943  supaddc  30009  abrexdom  30189  heiborlem10  30284  pellexlem3  30735  pell1234qrne0  30757  hbtlem6  31046  radcnvrat  31164  fzisoeu  31445  funressnfv  32047  faovcl  32119  cznnring  32464  zlmodzxznm  32808  3impexpbicom  32929  sb5ALT  33003  eexinst01  33004  ax6e2eq  33038  sineq0ALT  33445  bnj849  33690  bj-alequex  33982  bj-spimtv  33992  bj-axc15v  34042  bj-exlimmpi  34189  cvrnrefN  34709  pmod1i  35274  pmodN  35276  osumcllem11N  35392  pexmidlem8N  35403  pl42lem3N  35407  cdleme18b  35719  dochexmidlem8  36896  frege58b  37540
  Copyright terms: Public domain W3C validator