MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Structured 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  682  mp3an3  1349  merco2  1613  equs4v  1839  equcomi  1847  equviniv  1857  19.8aOLD  1913  aev  2003  spimt  2064  equs4  2093  ax12v2  2143  2ax6elem  2249  pm13.183  3147  sbcth  3250  sbcth2  3319  ssun3  3567  ssun4  3568  uneqdifeq  3822  ralf0  3842  uniintsn  4229  rext  4605  exss  4620  uniopel  4660  wefrc  4783  relop  4940  dmrnssfld  5048  iss  5107  sofld  5239  relcoi1OLD  5320  ordun  5479  nfunv  5568  funimass2  5611  fvbr0  5839  fvmptg  5899  fovcl  6352  ov3  6384  elovmpt2  6465  limsssuc  6628  tfisi  6636  finds1  6673  frxp  6854  wfrlem5  6988  wfrlem16  6999  dfrecs3  7039  tfrlem1  7042  oaordi  7195  oaword2  7202  omeulem1  7231  oeworde  7242  oelim2  7244  nnaordi  7267  oaabs2  7294  0domg  7645  limenpsi  7693  enp1i  7752  findcard2  7757  ordunifi  7767  fidomdm  7799  dffi3  7891  oismo  8001  wdom2d  8041  wdomima2g  8047  suc11reg  8070  elom3  8099  cantnfval2  8119  rankunb  8266  rankval4  8283  karden  8311  cardsn  8348  cardlim  8351  cardprclem  8358  fseqdom  8401  dfac12lem3  8519  kmlem2  8525  kmlem10  8533  cflim2  8637  cfslb2n  8642  fin23lem27  8702  axcc3  8812  axcc4  8813  acncc  8814  domtriomlem  8816  axdclem2  8894  imadomg  8906  alephval2  8941  alephreg  8951  axextnd  8960  fpwwe2lem10  9008  pwfseq  9033  gch2  9044  axgroth3  9200  inaprc  9205  nlt1pi  9275  indpi  9276  1re  9586  mul02lem2  9754  addid1  9757  fimaxre  10495  supaddc  10518  supmul1  10520  inelr  10543  rimul  10544  nnge1  10579  zneo  10962  ltweuz  12118  hashrabsn1  12496  hashf1lem2  12560  hash2pwpr  12576  climuni  13552  fsum2d  13768  fsumabs  13797  fsumrlim  13807  fsumo1  13808  fsumiun  13817  fprod2d  13971  efne0  14087  ruclem13  14230  dvdslelem  14285  divalglem0  14307  lcmfnnval  14530  lcmfnnvalOLD  14533  prmreclem2  14797  prmreclem3  14798  mreexexd  15490  coaval  15899  xpcco  16004  pltirr  16145  frgpnabllem1  17445  ablfac1eulem  17641  mdetunilem9  19580  mretopd  20043  fiuncmp  20354  ptcmpfi  20763  filtop  20805  supnfcls  20970  flimfnfcls  20978  alexsubALTlem2  20998  alexsubALTlem4  21000  trust  21179  rectbntr0  21785  fsumcn  21837  ovoliunlem3  22392  ovolicc2lem4OLD  22408  ovolicc2lem4  22409  dyadmax  22491  vitali  22506  itgfsum  22719  dvmptfsum  22862  fta1g  23053  fta1  23196  aannenlem1  23219  aalioulem3  23225  logltb  23484  logdmn0  23520  ang180lem2  23674  angpined  23691  mumullem2  24042  dchrisum0re  24286  chpdifbnd  24328  pntrlog2bnd  24357  pntibndlem3  24365  pnt3  24385  nbgraop  25086  isuvtx  25151  0eusgraiff0rgra  25602  frgrancvvdeqlem4  25696  dvrunz  26096  hiidge0  26686  chsupval  26923  chsupcl  26928  chsupss  26930  ococin  26996  chsupval2  26998  ssjo  27035  h1de2i  27141  pjss2i  27268  pjssmii  27269  sto2i  27825  stge1i  27826  stle0i  27827  stlei  27828  stlesi  27829  stm1i  27831  staddi  27834  stadd3i  27836  golem1  27859  stcltrlem1  27864  mdexchi  27923  chirred  27983  atabsi  27989  rmoeqALT  28058  abrexdomjm  28077  ifbieq12d2  28098  iocinif  28306  voliune  28997  volfiniune  28998  probdif  29198  bnj849  29681  kur14lem9  29882  frrlem5  30462  nofv  30488  noprc  30512  sscoid  30622  limsucncmpi  31047  bj-alequex  31205  bj-spimtv  31215  bj-axc15v  31266  bj-exlimmpi  31418  finxpreclem4  31687  wl-embantALT  31748  wl-orel12  31750  wl-euequ1f  31804  wl-ax12v3  31813  poimirlem9  31850  abrexdom  31958  heiborlem10  32053  ax12eq  32418  ax12el  32419  ax12inda  32425  ax12v2-o  32426  cvrnrefN  32754  pmod1i  33319  pmodN  33321  osumcllem11N  33437  pexmidlem8N  33448  pl42lem3N  33452  cdleme18b  33764  dochexmidlem8  34941  pellexlem3  35582  pell1234qrne0  35606  hbtlem6  35895  radcnvrat  36570  3impexpbicom  36741  sb5ALT  36789  eexinst01  36790  ax6e2eq  36831  sineq0ALT  37244  fzisoeu  37409  ovnsubaddlem2  38234  funressnfv  38437  faovcl  38509  mod2eq1n2dvds  38532  propssopi  38803  funsndifnop  38822  nbgrval  39136  cznnring  39543  zlmodzxznm  39877  nn0o1gt2  39914  elbigolo1  39955  dignn0flhalflem1  40013  nn0sumshdig  40021
  Copyright terms: Public domain W3C validator