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. Inference associated with com12 31. (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  676  mp3an3  1311  merco2  1573  equs4v  1792  equcomi  1798  equviniv  1808  19.8aOLD  1863  aev  1948  spimt  2010  equs4  2039  ax12v2  2087  2ax6elem  2195  ax12eq  2273  ax12el  2274  ax12inda  2280  ax12v2-o  2281  pm13.183  3237  sbcth  3339  sbcth2  3408  ssun3  3655  ssun4  3656  uneqdifeq  3904  ralf0  3924  uniintsn  4309  rext  4685  exss  4700  uniopel  4740  wefrc  4862  ordun  4968  relop  5142  dmrnssfld  5250  iss  5309  sofld  5439  relcoi1  5519  nfunv  5601  funimass2  5644  fvbr0  5869  fvmptg  5929  fovcl  6380  ov3  6412  elovmpt2  6493  limsssuc  6658  tfisi  6666  finds1  6702  frxp  6883  tfrlem1  7037  oaordi  7187  oaword2  7194  omeulem1  7223  oeworde  7234  oelim2  7236  nnaordi  7259  oaabs2  7286  0domg  7637  limenpsi  7685  enp1i  7747  findcard2  7752  ordunifi  7762  fidomdm  7794  dffi3  7883  oismo  7957  wdom2d  7998  wdomima2g  8004  suc11reg  8027  elom3  8056  cantnfval2  8079  cantnfval2OLD  8109  rankunb  8259  rankval4  8276  karden  8304  cardsn  8341  cardlim  8344  cardprclem  8351  fseqdom  8398  dfac12lem3  8516  kmlem2  8522  kmlem10  8530  cflim2  8634  cfslb2n  8639  fin23lem27  8699  axcc3  8809  axcc4  8810  acncc  8811  domtriomlem  8813  axdclem2  8891  imadomg  8903  alephval2  8938  alephreg  8948  axextnd  8957  fpwwe2lem10  9006  pwfseq  9031  gch2  9042  axgroth3  9198  inaprc  9203  nlt1pi  9273  indpi  9274  1re  9584  mul02lem2  9746  addid1  9749  fimaxre  10485  supmul1  10503  inelr  10521  rimul  10522  nnge1  10557  zneo  10941  uzindOLD  10953  ltweuz  12057  hashrabsn1  12428  hashf1lem2  12492  hash2pwpr  12506  climuni  13460  fsum2d  13671  fsumabs  13700  fsumrlim  13710  fsumo1  13711  fsumiun  13720  fprod2d  13870  efne0  13917  ruclem13  14062  dvdslelem  14117  divalglem0  14138  prmreclem2  14522  prmreclem3  14523  mreexexd  15140  coaval  15549  xpcco  15654  pltirr  15795  frgpnabllem1  17079  ablfac1eulem  17321  mdetunilem9  19292  mretopd  19763  fiuncmp  20074  ptcmpfi  20483  filtop  20525  supnfcls  20690  flimfnfcls  20698  alexsubALTlem2  20717  alexsubALTlem4  20719  trust  20901  rectbntr0  21506  fsumcn  21543  ovoliunlem3  22084  ovolicc2lem4  22100  dyadmax  22176  vitali  22191  itgfsum  22402  dvmptfsum  22545  fta1g  22737  fta1  22873  aannenlem1  22893  aalioulem3  22899  logltb  23156  logdmn0  23192  ang180lem2  23344  angpined  23361  mumullem2  23655  dchrisum0re  23899  chpdifbnd  23941  pntrlog2bnd  23970  pntibndlem3  23978  pnt3  23998  nbgraop  24628  isuvtx  24693  0eusgraiff0rgra  25144  frgrancvvdeqlem4  25238  dvrunz  25636  hiidge0  26216  chsupval  26454  chsupcl  26459  chsupss  26461  ococin  26527  chsupval2  26529  ssjo  26566  h1de2i  26672  pjss2i  26799  pjssmii  26800  sto2i  27357  stge1i  27358  stle0i  27359  stlei  27360  stlesi  27361  stm1i  27363  staddi  27366  stadd3i  27368  golem1  27391  stcltrlem1  27396  mdexchi  27455  chirred  27515  atabsi  27521  rmoeq  27587  abrexdomjm  27607  ifbieq12d2  27629  iocinif  27829  voliune  28441  volfiniune  28442  probdif  28626  kur14lem9  28925  wfrlem5  29590  wfrlem16  29601  frrlem5  29634  nofv  29660  noprc  29684  sscoid  29794  limsucncmpi  30141  wl-embantALT  30210  wl-orel12  30212  supaddc  30284  abrexdom  30464  heiborlem10  30559  pellexlem3  31009  pell1234qrne0  31031  hbtlem6  31322  radcnvrat  31439  fzisoeu  31742  funressnfv  32455  faovcl  32527  mod2eq1n2dvds  32537  cznnring  33037  zlmodzxznm  33371  nn0o1gt2  33410  elbigolo1  33451  dignn0flhalflem1  33509  nn0sumshdig  33517  3impexpbicom  33627  sb5ALT  33701  eexinst01  33702  ax6e2eq  33743  sineq0ALT  34157  bnj849  34403  bj-alequex  34688  bj-spimtv  34698  bj-axc15v  34750  bj-exlimmpi  34897  cvrnrefN  35423  pmod1i  35988  pmodN  35990  osumcllem11N  36106  pexmidlem8N  36117  pl42lem3N  36121  cdleme18b  36433  dochexmidlem8  37610
  Copyright terms: Public domain W3C validator