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  1313  merco2  1553  equcomi  1742  equviniv  1752  19.8a  1806  19.8aOLD  1807  aev  1890  spimt  1974  equs4  2008  ax12v2  2056  2ax6elem  2179  ax12eq  2264  ax12el  2265  ax12inda  2271  ax12v2-o  2272  pm13.183  3244  sbcth  3346  sbcth2  3426  ssun3  3669  ssun4  3670  uneqdifeq  3915  ralf0  3934  uniintsn  4319  rext  4695  exss  4710  uniopel  4751  wefrc  4873  ordun  4979  relop  5153  dmrnssfld  5261  iss  5321  sofld  5455  relcoi1  5536  nfunv  5619  funimass2  5662  fvbr0  5887  fvmptg  5948  fovcl  6391  ov3  6423  elovmpt2  6504  limsssuc  6669  tfisi  6677  finds1  6713  frxp  6893  tfrlem1  7045  oaordi  7195  oaword2  7202  omeulem1  7231  oeworde  7242  oelim2  7244  nnaordi  7267  oaabs2  7294  0domg  7644  limenpsi  7692  enp1i  7755  findcard2  7760  ordunifi  7770  fidomdm  7802  dffi3  7891  oismo  7965  wdom2d  8006  wdomima2g  8012  suc11reg  8036  elom3  8065  cantnfval2  8088  cantnfval2OLD  8118  rankunb  8268  rankval4  8285  karden  8313  cardsn  8350  cardlim  8353  cardprclem  8360  fseqdom  8407  dfac12lem3  8525  kmlem2  8531  kmlem10  8539  cflim2  8643  cfslb2n  8648  fin23lem27  8708  axcc3  8818  axcc4  8819  acncc  8820  domtriomlem  8822  axdclem2  8900  imadomg  8912  alephval2  8947  alephreg  8957  axextnd  8966  fpwwe2lem10  9017  pwfseq  9042  gch2  9053  axgroth3  9209  inaprc  9214  nlt1pi  9284  indpi  9285  1re  9595  mul02lem2  9756  addid1  9759  fimaxre  10490  supmul1  10508  inelr  10526  rimul  10527  nnge1  10562  zneo  10943  uzindOLD  10955  ltweuz  12040  hashrabsn1  12410  hashf1lem2  12471  hash2pwpr  12485  climuni  13338  fsum2d  13549  fsumabs  13578  fsumrlim  13588  fsumo1  13589  fsumiun  13598  efne0  13693  ruclem13  13836  dvdslelem  13889  divalglem0  13910  prmreclem2  14294  prmreclem3  14295  mreexexd  14903  coaval  15253  xpcco  15310  pltirr  15450  frgpnabllem1  16680  ablfac1eulem  16925  mdetunilem9  18917  mretopd  19387  fiuncmp  19698  ptcmpfi  20077  filtop  20119  supnfcls  20284  flimfnfcls  20292  alexsubALTlem2  20311  alexsubALTlem4  20313  trust  20495  rectbntr0  21100  fsumcn  21137  ovoliunlem3  21678  ovolicc2lem4  21694  dyadmax  21770  vitali  21785  itgfsum  21996  dvmptfsum  22139  fta1g  22331  fta1  22466  aannenlem1  22486  aalioulem3  22492  logltb  22740  logdmn0  22777  ang180lem2  22898  angpined  22917  mumullem2  23210  dchrisum0re  23454  chpdifbnd  23496  pntrlog2bnd  23525  pntibndlem3  23533  pnt3  23553  nbgraop  24127  isuvtx  24192  0eusgraiff0rgra  24643  frgrancvvdeqlem4  24738  dvrunz  25139  hiidge0  25719  chsupval  25957  chsupcl  25962  chsupss  25964  ococin  26030  chsupval2  26032  ssjo  26069  h1de2i  26175  pjss2i  26302  pjssmii  26303  sto2i  26860  stge1i  26861  stle0i  26862  stlei  26863  stlesi  26864  stm1i  26866  staddi  26869  stadd3i  26871  golem1  26894  stcltrlem1  26899  mdexchi  26958  chirred  27018  atabsi  27024  rmoeq  27090  abrexdomjm  27107  ifbieq12d2  27122  iocinif  27288  voliune  27869  volfiniune  27870  sibfof  27950  probdif  28027  kur14lem9  28326  relexp1  28557  fprod2d  28716  wfrlem5  28952  wfrlem16  28963  frrlem5  28996  nofv  29022  noprc  29046  sscoid  29168  limsucncmpi  29515  wl-embantALT  29580  supaddc  29646  abrexdom  29852  heiborlem10  29947  pellexlem3  30399  pell1234qrne0  30421  hbtlem6  30710  funressnfv  31708  faovcl  31780  zlmodzxznm  32197  3impexpbicom  32318  sb5ALT  32392  eexinst01  32393  ax6e2eq  32428  sineq0ALT  32835  bnj849  33080  bj-alequex  33368  bj-spimtv  33378  bj-equs4v  33409  bj-axc15v  33429  bj-exlimmpi  33576  cvrnrefN  34097  pmod1i  34662  pmodN  34664  osumcllem11N  34780  pexmidlem8N  34791  pl42lem3N  34795  cdleme18b  35106  dochexmidlem8  36282  frege58b  36910
  Copyright terms: Public domain W3C validator