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

Theorem mp2b 9
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 8 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  eqvinc  2897  elnn  4668  intasym  5060  relcoi1  5203  funres11  5322  cnvresid  5324  fparlem1  6220  fparlem2  6221  dftpos4  6255  tposf12  6261  tfr2b  6414  tz7.44lem1  6420  xpcomco  6954  sbthlem2  6974  fidomdm  7140  marypha1lem  7188  hartogslem1  7259  brwdom2  7289  inf3lem6  7336  omex  7346  cantnfdm  7367  cantnfval  7371  cantnff  7377  cnfcom  7405  cnfcom2  7407  cnfcom3lem  7408  cnfcom3  7409  tz9.1c  7414  r1tr  7450  r1ord3g  7453  rankwflemb  7467  r1elwf  7470  r1elss  7480  rankval3b  7500  onssr1  7505  infxpenlem  7643  alephnbtwn  7700  alephordilem1  7702  alephfp  7737  dfac13  7770  pwsdompw  7832  infcdaabs  7834  ackbij1  7866  ackbij2  7871  r1om  7872  cflim2  7891  fin23lem27  7956  fin23lem29  7969  fin23lem30  7970  fin1a2lem6  8033  fin1a2lem7  8034  fin1a2lem13  8040  itunitc1  8048  itunitc  8049  ituniiun  8050  hsmexlem5  8058  axcc2lem  8064  axcc3  8066  zorn2lem6  8130  zorn2lem7  8131  ttukeylem6  8143  axdc  8150  fodom  8151  iunfo  8163  cardval  8170  cardid  8171  pwcfsdom  8207  alephom  8209  fpwwe  8270  canthp1lem2  8277  canthp1  8278  gchaleph2  8300  r1limwun  8360  inaprc  8460  nqerf  8556  recmulnq  8590  dmrecnq  8594  halfnq  8602  genpdm  8628  reclem3pr  8675  axresscn  8772  axpre-sup  8793  1re  8839  0re  8840  00id  8989  addid1  8994  renegcli  9110  zexALT  10044  uzn0  10245  dfle2  10483  xrinfmss  10630  axdc4uzlem  11046  facnn  11292  fac0  11293  hashgval  11342  hashinf  11344  hashp1i  11371  hashxplem  11387  cats1fv  11511  cnrecnv  11652  rexanuz  11831  climdm  12030  lo1eq  12044  rlimeq  12045  sumsn  12215  tanval  12410  rpnnen2lem11  12505  rpnnen  12507  sadadd2lem  12652  sadadd3  12654  sadaddlem  12659  sadasslem  12663  sadeq  12665  3prm  12777  unbenlem  12957  prmreclem6  12970  vdwlem8  13037  vdwnnlem1  13044  0ram  13069  structcnvcnv  13161  prdsval  13357  prdsbas  13359  prdsplusg  13360  prdsmulr  13361  prdsvsca  13362  prdshom  13368  xpsfrn  13473  xpsff1o2  13475  catcoppccl  13942  catcfuccl  13943  catcxpccl  13983  tsrss  14334  symgid  14783  efgmnvl  15025  efgval  15028  efgi0  15031  efgi1  15032  efgredeu  15063  0frgp  15090  lt6abl  15183  gsumval3  15193  gsumzres  15196  gsumzadd  15206  gsum2d  15225  dprdfadd  15257  dprdres  15265  dmdprdsplit2lem  15282  isdrng2  15524  drngmcl  15527  drngid2  15530  psrplusg  16128  coe1sfi  16295  ply1plusgfvi  16322  cnfldplusf  16403  cnfldsub  16404  cnsubmlem  16421  cnmsubglem  16436  gzrngunitlem  16438  mulgghm2  16461  zzngim  16508  pjfval  16608  pjpm  16610  indistpsALT  16752  tgrest  16892  leordtval2  16944  lmbr2  16991  cnprest  17019  lmff  17031  kgenidm  17244  tx1cn  17305  tx2cn  17306  hausdiag  17341  tsmsres  17828  xmetge0  17911  qdensere  18281  cnblcld  18286  cnfldms  18287  cnfldtopn  18293  xrsdsre  18318  xrge0tsms  18341  iccpnfcnv  18444  xrhmeo  18446  cnheiborlem  18454  lmmbr2  18687  lmcau  18740  cmetss  18742  cncms  18776  ovolctb  18851  ovoliunnul  18868  ismbl  18887  volf  18890  voliunlem1  18909  ioorf  18930  ioorinv  18933  ioorcl  18934  dyaddisj  18953  dyadmax  18955  dyadmbl  18957  mbfid  18993  ismbfd  18997  mbfimaopnlem  19012  limcresi  19237  dvreslem  19261  dvres2lem  19262  dvcjbr  19300  dvferm1  19334  dvferm2  19336  dvlip2  19344  dv11cn  19350  tdeglem4  19448  deg1ldg  19480  deg1leb  19483  plycpn  19671  vieta1lem2  19693  elqaa  19704  aalioulem2  19715  aaliou3lem3  19726  aaliou3lem4  19728  pserulm  19800  psercnlem2  19802  psercnlem1  19803  psercn  19804  abelth  19819  reeff1o  19825  pilem1  19829  efhalfpi  19841  coseq0negpitopi  19873  pige3  19887  efif1olem3  19908  efif1olem4  19909  efifo  19911  eff1olem  19912  logrn  19918  ellogrn  19919  relogf1o  19926  argregt0  19966  argrege0  19967  dvrelog  19986  dvloglem  19997  logf1o2  19999  dvlog  20000  efopnlem1  20005  efopnlem2  20006  logtayl  20009  cxpcn3lem  20089  cxpcn3  20090  resqrcn  20091  asinneg  20184  asinrebnd  20199  atan0  20206  atanbnd  20224  areambl  20255  sqrlim  20269  amgmlem  20286  basellem1  20320  basellem4  20323  sqff1o  20422  dchrplusg  20488  bposlem6  20530  bposlem8  20532  lgseisenlem4  20593  dchrvmasumlem2  20649  dchrisum0flblem1  20659  mulog2sum  20688  pntibndlem1  20740  pntlemo  20758  qrng0  20772  ostth  20790  grporn  20881  issubgoi  20979  gidsn  21017  ginvsn  21018  rngomndo  21090  ip0i  21405  ubthlem1  21451  ubthlem2  21452  axhcompl-zf  21580  normlem7  21697  bcseqi  21701  bcsiALT  21760  hlimf  21819  hlimuni  21820  hhshsslem1  21846  hhsssh  21848  hhsscms  21858  occllem  21884  occl  21885  h1deoi  22130  h1dei  22131  h1de2ctlem  22136  h1de2ci  22137  spansni  22138  spanunsni  22160  pjpythi  22303  nmopadjlem  22671  adjcoi  22682  nmopcoadji  22683  pjoccoi  22760  shatomistici  22943  ballotlem1  23047  ceqsexv2d  23164  cntnevol  23177  xppreima  23213  iistmd  23288  xpinpreima  23292  xpinpreima2  23293  tpr2rico  23298  mndpluscn  23301  xrge0pluscn  23324  xrge0neqmnf  23332  dmct  23344  gsumpropd2lem  23381  xrge0tsmsd  23384  brsiga  23516  1stmbfm  23567  2ndmbfm  23568  br2base  23576  indf1ofs  23611  dstrvprob  23674  coinflipspace  23683  coinfliprv  23685  coinflippv  23686  iccllyscon  23783  rellyscon  23784  vdegp1ai  23910  dfrdg2  24154  omsinds  24221  trpredlem1  24232  trpredtr  24235  trpredmintr  24236  wfrlem14  24271  dfrdg4  24490  elhf  24806  limsucncmpi  24886  areacirc  24942  scprefat  25082  scprefat2  25083  domrancur1c  25213  bsi  25512  limptlimpr2lem2  25586  dtt1  25599  intrn  25610  bsi2  25650  bsi3  25652  bsi4  25654  addcanri  25677  issrc  25878  tartarmap  25899  prismorcsetlemc  25928  idcatfun  25952  lemindclsbu  26006  pgapspf  26063  pdiveql  26179  filnetlem3  26340  fdc  26466  ismrer1  26573  reheibor  26574  2rexfrabdioph  26888  3rexfrabdioph  26889  4rexfrabdioph  26890  6rexfrabdioph  26891  7rexfrabdioph  26892  rencldnfi  26915  jm2.27dlem2  27114  wepwso  27150  dfac11  27171  pwssplit4  27202  frlmpwfi  27273  isnumbasgrplem3  27281  mpaaeu  27366  mvdco  27399  proot1mul  27526  proot1hash  27530  seff  27549  sumsnd  27708  stoweidlem34  27794  stoweidlem37  27797  bi123imp0  28317  tendo0co2  31050  erng1r  31257  dvalveclem  31288  dva0g  31290  dvh0g  31374
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator