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

Theorem mp2b 11
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
Hypotheses
Ref Expression
mp2b.1  |-  ph
mp2b.2  |-  ( ph  ->  ps )
mp2b.3  |-  ( ps 
->  ch )
Assertion
Ref Expression
mp2b  |-  ch

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3  |-  ph
2 mp2b.2 . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 10 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 10 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  eqvinc  2846  elnn  4603  intasym  5011  relcoi1  5153  funres11  5223  cnvresid  5225  fvex  5437  fparlem1  6117  fparlem2  6118  dftpos4  6152  tposf12  6158  tfr2b  6345  tz7.44lem1  6351  xpcomco  6885  sbthlem2  6905  fidomdm  7071  marypha1lem  7119  hartogslem1  7190  brwdom2  7220  inf3lem6  7267  omex  7277  cantnfdm  7298  cantnfval  7302  cantnff  7308  cnfcom  7336  cnfcom2  7338  cnfcom3lem  7339  cnfcom3  7340  tz9.1c  7345  r1tr  7381  r1ord3g  7384  rankwflemb  7398  r1elwf  7401  r1elss  7411  rankval3b  7431  onssr1  7436  infxpenlem  7574  alephnbtwn  7631  alephordilem1  7633  alephfp  7668  dfac13  7701  pwsdompw  7763  infcdaabs  7765  ackbij1  7797  ackbij2  7802  r1om  7803  cflim2  7822  fin23lem27  7887  fin23lem29  7900  fin23lem30  7901  fin1a2lem6  7964  fin1a2lem7  7965  fin1a2lem13  7971  itunitc1  7979  itunitc  7980  ituniiun  7981  hsmexlem5  7989  axcc2lem  7995  axcc3  7997  zorn2lem6  8061  zorn2lem7  8062  ttukeylem6  8074  axdc  8081  fodom  8082  iunfo  8094  cardval  8101  cardid  8102  pwcfsdom  8138  alephom  8140  fpwwe  8201  canthp1lem2  8208  canthp1  8209  gchaleph2  8231  r1limwun  8291  inaprc  8391  nqerf  8487  recmulnq  8521  dmrecnq  8525  halfnq  8533  genpdm  8559  reclem3pr  8606  axresscn  8703  axpre-sup  8724  1re  8770  0re  8771  00id  8920  addid1  8925  renegcli  9041  zexALT  9974  uzn0  10175  dfle2  10413  xrinfmss  10559  axdc4uzlem  10975  facnn  11221  fac0  11222  hashgval  11271  hashinf  11273  hashp1i  11299  hashxplem  11315  cats1fv  11439  cnrecnv  11580  rexanuz  11759  climdm  11958  lo1eq  11972  rlimeq  11973  sumsn  12143  tanval  12335  rpnnen2lem11  12430  rpnnen  12432  sadadd2lem  12577  sadadd3  12579  sadaddlem  12584  sadasslem  12588  sadeq  12590  3prm  12702  unbenlem  12882  prmreclem6  12895  vdwlem8  12962  vdwnnlem1  12969  0ram  12994  structcnvcnv  13086  prdsval  13282  prdsbas  13284  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  prdshom  13293  xpsfrn  13398  xpsff1o2  13400  catcoppccl  13867  catcfuccl  13868  catcxpccl  13908  tsrss  14259  symgid  14708  efgmnvl  14950  efgval  14953  efgi0  14956  efgi1  14957  efgredeu  14988  0frgp  15015  lt6abl  15108  gsumval3  15118  gsumzres  15121  gsumzadd  15131  gsum2d  15150  dprdfadd  15182  dprdres  15190  dmdprdsplit2lem  15207  isdrng2  15449  drngmcl  15452  drngid2  15455  psrplusg  16053  coe1sfi  16220  ply1plusgfvi  16247  cnfldplusf  16328  cnfldsub  16329  cnsubmlem  16346  cnmsubglem  16361  gzrngunitlem  16363  mulgghm2  16386  zzngim  16433  pjfval  16533  pjpm  16535  indistpsALT  16677  tgrest  16817  leordtval2  16869  lmbr2  16916  cnprest  16944  lmff  16956  kgenidm  17169  tx1cn  17230  tx2cn  17231  hausdiag  17266  tsmsres  17753  xmetge0  17836  qdensere  18206  cnblcld  18211  cnfldms  18212  cnfldtopn  18218  xrsdsre  18243  xrge0tsms  18266  iccpnfcnv  18369  xrhmeo  18371  cnheiborlem  18379  lmmbr2  18612  lmcau  18665  cmetss  18667  cncms  18701  ovolctb  18776  ovoliunnul  18793  ismbl  18812  volf  18815  voliunlem1  18834  ioorf  18855  ioorinv  18858  ioorcl  18859  dyaddisj  18878  dyadmax  18880  dyadmbl  18882  mbfid  18918  ismbfd  18922  mbfimaopnlem  18937  limcresi  19162  dvreslem  19186  dvres2lem  19187  dvcjbr  19225  dvferm1  19259  dvferm2  19261  dvlip2  19269  dv11cn  19275  tdeglem4  19373  deg1ldg  19405  deg1leb  19408  plycpn  19596  vieta1lem2  19618  elqaa  19629  aalioulem2  19640  aaliou3lem3  19651  aaliou3lem4  19653  pserulm  19725  psercnlem2  19727  psercnlem1  19728  psercn  19729  abelth  19744  reeff1o  19750  pilem1  19754  efhalfpi  19766  coseq0negpitopi  19798  pige3  19812  efif1olem3  19833  efif1olem4  19834  efifo  19836  eff1olem  19837  logrn  19843  ellogrn  19844  relogf1o  19851  argregt0  19891  argrege0  19892  dvrelog  19911  dvloglem  19922  logf1o2  19924  dvlog  19925  efopnlem1  19930  efopnlem2  19931  logtayl  19934  cxpcn3lem  20014  cxpcn3  20015  resqrcn  20016  asinneg  20109  asinrebnd  20124  atan0  20131  atanbnd  20149  areambl  20180  sqrlim  20194  amgmlem  20211  basellem1  20245  basellem4  20248  sqff1o  20347  dchrplusg  20413  bposlem6  20455  bposlem8  20457  lgseisenlem4  20518  dchrvmasumlem2  20574  dchrisum0flblem1  20584  mulog2sum  20613  pntibndlem1  20665  pntlemo  20683  qrng0  20697  ostth  20715  grporn  20804  issubgoi  20902  gidsn  20940  ginvsn  20941  rngomndo  21013  ip0i  21328  ubthlem1  21374  ubthlem2  21375  axhcompl-zf  21503  normlem7  21620  bcseqi  21624  bcsiALT  21683  hlimf  21742  hlimuni  21743  hhshsslem1  21769  hhsssh  21771  hhsscms  21781  occllem  21807  occl  21808  h1deoi  22053  h1dei  22054  h1de2ctlem  22059  h1de2ci  22060  spansni  22061  spanunsni  22083  pjpythi  22244  nmopadjlem  22594  adjcoi  22605  nmopcoadji  22606  pjoccoi  22683  shatomistici  22866  ballotlem1  22971  iccllyscon  23118  rellyscon  23119  vdegp1ai  23245  dfrdg2  23486  omsinds  23553  trpredlem1  23564  trpredtr  23567  trpredmintr  23568  wfrlem14  23603  dfrdg4  23828  elhf  24144  limsucncmpi  24224  scprefat  24402  scprefat2  24403  repfuntw  24492  domrancur1c  24534  bsi  24833  limptlimpr2lem2  24907  dtt1  24920  intrn  24931  bsi2  24971  bsi3  24973  bsi4  24975  addcanri  24998  issrc  25199  tartarmap  25220  prismorcsetlemc  25249  idcatfun  25273  lemindclsbu  25327  pgapspf  25384  pdiveql  25500  filnetlem3  25661  fdc  25787  ismrer1  25894  reheibor  25895  2rexfrabdioph  26209  3rexfrabdioph  26210  4rexfrabdioph  26211  6rexfrabdioph  26212  7rexfrabdioph  26213  rencldnfi  26236  jm2.27dlem2  26435  wepwso  26471  dfac11  26492  pwssplit4  26523  frlmpwfi  26594  isnumbasgrplem3  26602  mpaaeu  26687  mvdco  26720  proot1mul  26847  proot1hash  26851  seff  26870  sumsnd  27030  stoweidlem34  27083  stoweidlem37  27086  tendo0co2  30107  erng1r  30314  dvalveclem  30345  dva0g  30347  dvh0g  30431
This theorem was proved from axioms:  ax-mp 10
  Copyright terms: Public domain W3C validator