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

Theorem mp2b 10
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  3055  elnn  4847  intasym  5241  relcoi1  5390  funres11  5513  cnvresid  5515  fparlem1  6438  fparlem2  6439  dftpos4  6490  tposf12  6496  tfr2b  6649  tz7.44lem1  6655  xpcomco  7190  sbthlem2  7210  fidomdm  7380  marypha1lem  7430  hartogslem1  7503  brwdom2  7533  inf3lem6  7580  omex  7590  cantnfdm  7611  cantnfval  7615  cantnff  7621  cnfcom  7649  cnfcom2  7651  cnfcom3lem  7652  cnfcom3  7653  tz9.1c  7658  r1tr  7694  r1ord3g  7697  rankwflemb  7711  r1elwf  7714  r1elss  7724  rankval3b  7744  onssr1  7749  infxpenlem  7887  alephnbtwn  7944  alephordilem1  7946  alephfp  7981  dfac13  8014  pwsdompw  8076  infcdaabs  8078  ackbij1  8110  ackbij2  8115  r1om  8116  cflim2  8135  fin23lem27  8200  fin23lem29  8213  fin23lem30  8214  fin1a2lem6  8277  fin1a2lem7  8278  fin1a2lem13  8284  itunitc1  8292  itunitc  8293  ituniiun  8294  hsmexlem5  8302  axcc2lem  8308  axcc3  8310  zorn2lem6  8373  zorn2lem7  8374  ttukeylem6  8386  axdc  8393  fodom  8394  iunfo  8406  cardval  8413  cardid  8414  pwcfsdom  8450  alephom  8452  fpwwe  8513  canthp1lem2  8520  canthp1  8521  gchaleph2  8543  r1limwun  8603  inaprc  8703  nqerf  8799  recmulnq  8833  dmrecnq  8837  halfnq  8845  genpdm  8871  reclem3pr  8918  axresscn  9015  axpre-sup  9036  1re  9082  0re  9083  00id  9233  addid1  9238  renegcli  9354  zexALT  10292  uzn0  10493  dfle2  10732  xrinfmss  10880  axdc4uzlem  11313  facnn  11560  fac0  11561  hashgval  11613  hashinf  11615  hashrabrsn  11640  hashp1i  11664  hashxplem  11688  brfi1uzind  11707  cats1fv  11815  cnrecnv  11962  rexanuz  12141  climdm  12340  lo1eq  12354  rlimeq  12355  sumsn  12526  tanval  12721  rpnnen2lem11  12816  rpnnen  12818  sadadd2lem  12963  sadadd3  12965  sadaddlem  12970  sadasslem  12974  sadeq  12976  3prm  13088  unbenlem  13268  prmreclem6  13281  vdwlem8  13348  vdwnnlem1  13355  0ram  13380  structcnvcnv  13472  prdsval  13670  prdsbas  13672  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  prdshom  13681  xpsfrn  13786  xpsff1o2  13788  catcoppccl  14255  catcfuccl  14256  catcxpccl  14296  tsrss  14647  symgid  15096  efgmnvl  15338  efgval  15341  efgi0  15344  efgi1  15345  efgredeu  15376  0frgp  15403  lt6abl  15496  gsumval3  15506  gsumzres  15509  gsumzadd  15519  gsum2d  15538  dprdfadd  15570  dprdres  15578  dmdprdsplit2lem  15595  isdrng2  15837  drngmcl  15840  drngid2  15843  psrplusg  16437  coe1sfi  16602  ply1plusgfvi  16628  cnfldplusf  16720  cnfldsub  16721  cnsubmlem  16738  cnmsubglem  16753  gzrngunitlem  16755  mulgghm2  16778  zzngim  16825  pjfval  16925  pjpm  16927  indistpsALT  17069  tgrest  17215  leordtval2  17268  lmbr2  17315  cnprest  17345  lmff  17357  kgenidm  17571  tx1cn  17633  tx2cn  17634  hausdiag  17669  tsmsres  18165  elrnust  18246  ustbas  18249  ustuqtop0  18262  utopsnneiplem  18269  neipcfilu  18318  psmetge0  18335  xmetge0  18366  qdensere  18796  cnblcld  18801  cnfldms  18802  cnfldtopn  18808  xrsdsre  18833  xrge0tsms  18857  iccpnfcnv  18961  xrhmeo  18963  cnheiborlem  18971  lmmbr2  19204  lmcau  19257  cmetss  19259  cncms  19301  cnfldcusp  19303  ovolctb  19378  ovoliunnul  19395  ismbl  19414  volf  19417  voliunlem1  19436  ioorf  19457  ioorinv  19460  ioorcl  19461  dyaddisj  19480  dyadmax  19482  dyadmbl  19484  mbfid  19520  ismbfd  19524  mbfimaopnlem  19539  limcresi  19764  dvreslem  19788  dvres2lem  19789  dvcjbr  19827  dvferm1  19861  dvferm2  19863  dvlip2  19871  dv11cn  19877  tdeglem4  19975  deg1ldg  20007  deg1leb  20010  plycpn  20198  vieta1lem2  20220  elqaa  20231  aalioulem2  20242  aaliou3lem3  20253  aaliou3lem4  20255  pserulm  20330  psercnlem2  20332  psercnlem1  20333  psercn  20334  abelth  20349  reeff1o  20355  pilem1  20359  efhalfpi  20371  coseq0negpitopi  20403  pige3  20417  tanregt0  20433  efif1olem3  20438  efif1olem4  20439  efifo  20441  eff1olem  20442  logrn  20448  ellogrn  20449  relogf1o  20456  argregt0  20497  argrege0  20498  dvrelog  20520  dvloglem  20531  logf1o2  20533  dvlog  20534  efopnlem1  20539  efopnlem2  20540  logtayl  20543  cxpcn3lem  20623  cxpcn3  20624  resqrcn  20625  asinneg  20718  asinrebnd  20733  atan0  20740  atanbnd  20758  areambl  20789  sqrlim  20803  amgmlem  20820  basellem1  20855  basellem4  20858  sqff1o  20957  dchrplusg  21023  bposlem6  21065  bposlem8  21067  lgseisenlem4  21128  dchrvmasumlem2  21184  dchrisum0flblem1  21194  mulog2sum  21223  pntibndlem1  21275  pntlemo  21293  qrng0  21307  ostth  21325  constr1trl  21580  vdegp1ai  21698  grporn  21792  issubgoi  21890  gidsn  21928  ginvsn  21929  rngomndo  22001  ip0i  22318  ubthlem1  22364  ubthlem2  22365  axhcompl-zf  22493  normlem7  22610  bcseqi  22614  bcsiALT  22673  hlimf  22732  hlimuni  22733  hhshsslem1  22759  hhsssh  22761  hhsscms  22771  occllem  22797  occl  22798  h1deoi  23043  h1dei  23044  h1de2ctlem  23049  h1de2ci  23050  spansni  23051  spanunsni  23073  pjpythi  23216  nmfn0  23482  nmopadjlem  23584  adjcoi  23595  nmopcoadji  23596  pjoccoi  23673  shatomistici  23856  ceqsexv2d  23977  imadifxp  24030  xppreima  24051  1stpreima  24087  2ndpreima  24088  dmct  24098  hashresfn  24148  xrge0neqmnf  24204  gsumpropd2lem  24212  xrge0tsmsd  24215  zzs0  24259  re0g  24265  iistmd  24292  xpinpreima  24296  xpinpreima2  24297  tpr2rico  24302  mndpluscn  24304  xrge0pluscn  24318  cnzh  24346  rezh  24347  zrhre  24377  qqhre  24378  rrhre  24379  sigaex  24484  brsiga  24529  cntnevol  24574  voliune  24577  1stmbfm  24602  2ndmbfm  24603  br2base  24611  dya2iocucvr  24626  dstrvprob  24721  coinflipspace  24730  coinfliprv  24732  coinflippv  24733  ballotlem1  24736  ballotlem8  24786  lgamucov  24814  iccllyscon  24929  rellyscon  24930  dfrdg2  25415  omsinds  25486  trpredlem1  25497  trpredtr  25500  trpredmintr  25501  wfrlem14  25543  dfrdg4  25787  imagesset  25790  elhf  26107  limsucncmpi  26187  ovoliunnfl  26238  voliunnfl  26240  mbfresfi  26243  itg2addnc  26249  ftc1anclem3  26272  areacirc  26288  filnetlem3  26400  fdc  26440  ismrer1  26538  reheibor  26539  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  rencldnfi  26873  jm2.27dlem2  27072  wepwso  27108  dfac11  27128  pwssplit4  27159  frlmpwfi  27230  isnumbasgrplem3  27238  mpaaeu  27323  mvdco  27356  proot1mul  27483  proot1hash  27487  seff  27506  sumsnd  27664  stoweidlem34  27750  stoweidlem37  27753  stirlinglem11  27800  stirlinglem12  27801  cshw1  28238  tendo0co2  31522  erng1r  31729  dvalveclem  31760  dva0g  31762  dvh0g  31846
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator