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  2908  elnn  4682  intasym  5074  relcoi1  5217  funres11  5336  cnvresid  5338  fparlem1  6234  fparlem2  6235  dftpos4  6269  tposf12  6275  tfr2b  6428  tz7.44lem1  6434  xpcomco  6968  sbthlem2  6988  fidomdm  7154  marypha1lem  7202  hartogslem1  7273  brwdom2  7303  inf3lem6  7350  omex  7360  cantnfdm  7381  cantnfval  7385  cantnff  7391  cnfcom  7419  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  tz9.1c  7428  r1tr  7464  r1ord3g  7467  rankwflemb  7481  r1elwf  7484  r1elss  7494  rankval3b  7514  onssr1  7519  infxpenlem  7657  alephnbtwn  7714  alephordilem1  7716  alephfp  7751  dfac13  7784  pwsdompw  7846  infcdaabs  7848  ackbij1  7880  ackbij2  7885  r1om  7886  cflim2  7905  fin23lem27  7970  fin23lem29  7983  fin23lem30  7984  fin1a2lem6  8047  fin1a2lem7  8048  fin1a2lem13  8054  itunitc1  8062  itunitc  8063  ituniiun  8064  hsmexlem5  8072  axcc2lem  8078  axcc3  8080  zorn2lem6  8144  zorn2lem7  8145  ttukeylem6  8157  axdc  8164  fodom  8165  iunfo  8177  cardval  8184  cardid  8185  pwcfsdom  8221  alephom  8223  fpwwe  8284  canthp1lem2  8291  canthp1  8292  gchaleph2  8314  r1limwun  8374  inaprc  8474  nqerf  8570  recmulnq  8604  dmrecnq  8608  halfnq  8616  genpdm  8642  reclem3pr  8689  axresscn  8786  axpre-sup  8807  1re  8853  0re  8854  00id  9003  addid1  9008  renegcli  9124  zexALT  10058  uzn0  10259  dfle2  10497  xrinfmss  10644  axdc4uzlem  11060  facnn  11306  fac0  11307  hashgval  11356  hashinf  11358  hashp1i  11385  hashxplem  11401  cats1fv  11525  cnrecnv  11666  rexanuz  11845  climdm  12044  lo1eq  12058  rlimeq  12059  sumsn  12229  tanval  12424  rpnnen2lem11  12519  rpnnen  12521  sadadd2lem  12666  sadadd3  12668  sadaddlem  12673  sadasslem  12677  sadeq  12679  3prm  12791  unbenlem  12971  prmreclem6  12984  vdwlem8  13051  vdwnnlem1  13058  0ram  13083  structcnvcnv  13175  prdsval  13371  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdshom  13382  xpsfrn  13487  xpsff1o2  13489  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997  tsrss  14348  symgid  14797  efgmnvl  15039  efgval  15042  efgi0  15045  efgi1  15046  efgredeu  15077  0frgp  15104  lt6abl  15197  gsumval3  15207  gsumzres  15210  gsumzadd  15220  gsum2d  15239  dprdfadd  15271  dprdres  15279  dmdprdsplit2lem  15296  isdrng2  15538  drngmcl  15541  drngid2  15544  psrplusg  16142  coe1sfi  16309  ply1plusgfvi  16336  cnfldplusf  16417  cnfldsub  16418  cnsubmlem  16435  cnmsubglem  16450  gzrngunitlem  16452  mulgghm2  16475  zzngim  16522  pjfval  16622  pjpm  16624  indistpsALT  16766  tgrest  16906  leordtval2  16958  lmbr2  17005  cnprest  17033  lmff  17045  kgenidm  17258  tx1cn  17319  tx2cn  17320  hausdiag  17355  tsmsres  17842  xmetge0  17925  qdensere  18295  cnblcld  18300  cnfldms  18301  cnfldtopn  18307  xrsdsre  18332  xrge0tsms  18355  iccpnfcnv  18458  xrhmeo  18460  cnheiborlem  18468  lmmbr2  18701  lmcau  18754  cmetss  18756  cncms  18790  ovolctb  18865  ovoliunnul  18882  ismbl  18901  volf  18904  voliunlem1  18923  ioorf  18944  ioorinv  18947  ioorcl  18948  dyaddisj  18967  dyadmax  18969  dyadmbl  18971  mbfid  19007  ismbfd  19011  mbfimaopnlem  19026  limcresi  19251  dvreslem  19275  dvres2lem  19276  dvcjbr  19314  dvferm1  19348  dvferm2  19350  dvlip2  19358  dv11cn  19364  tdeglem4  19462  deg1ldg  19494  deg1leb  19497  plycpn  19685  vieta1lem2  19707  elqaa  19718  aalioulem2  19729  aaliou3lem3  19740  aaliou3lem4  19742  pserulm  19814  psercnlem2  19816  psercnlem1  19817  psercn  19818  abelth  19833  reeff1o  19839  pilem1  19843  efhalfpi  19855  coseq0negpitopi  19887  pige3  19901  efif1olem3  19922  efif1olem4  19923  efifo  19925  eff1olem  19926  logrn  19932  ellogrn  19933  relogf1o  19940  argregt0  19980  argrege0  19981  dvrelog  20000  dvloglem  20011  logf1o2  20013  dvlog  20014  efopnlem1  20019  efopnlem2  20020  logtayl  20023  cxpcn3lem  20103  cxpcn3  20104  resqrcn  20105  asinneg  20198  asinrebnd  20213  atan0  20220  atanbnd  20238  areambl  20269  sqrlim  20283  amgmlem  20300  basellem1  20334  basellem4  20337  sqff1o  20436  dchrplusg  20502  bposlem6  20544  bposlem8  20546  lgseisenlem4  20607  dchrvmasumlem2  20663  dchrisum0flblem1  20673  mulog2sum  20702  pntibndlem1  20754  pntlemo  20772  qrng0  20786  ostth  20804  grporn  20895  issubgoi  20993  gidsn  21031  ginvsn  21032  rngomndo  21104  ip0i  21419  ubthlem1  21465  ubthlem2  21466  axhcompl-zf  21594  normlem7  21711  bcseqi  21715  bcsiALT  21774  hlimf  21833  hlimuni  21834  hhshsslem1  21860  hhsssh  21862  hhsscms  21872  occllem  21898  occl  21899  h1deoi  22144  h1dei  22145  h1de2ctlem  22150  h1de2ci  22151  spansni  22152  spanunsni  22174  pjpythi  22317  nmopadjlem  22685  adjcoi  22696  nmopcoadji  22697  pjoccoi  22774  shatomistici  22957  ballotlem1  23061  ceqsexv2d  23178  cntnevol  23191  xppreima  23226  iistmd  23301  xpinpreima  23305  xpinpreima2  23306  tpr2rico  23311  mndpluscn  23314  xrge0pluscn  23337  xrge0neqmnf  23345  dmct  23357  gsumpropd2lem  23394  xrge0tsmsd  23397  brsiga  23529  1stmbfm  23580  2ndmbfm  23581  br2base  23589  indf1ofs  23624  dstrvprob  23687  coinflipspace  23696  coinfliprv  23698  coinflippv  23699  iccllyscon  23796  rellyscon  23797  vdegp1ai  23923  dfrdg2  24223  omsinds  24290  trpredlem1  24301  trpredtr  24304  trpredmintr  24305  wfrlem14  24340  dfrdg4  24560  elhf  24876  limsucncmpi  24956  ovoliunnfl  25001  areacirc  25034  scprefat  25174  scprefat2  25175  domrancur1c  25305  bsi  25604  limptlimpr2lem2  25678  dtt1  25691  intrn  25702  bsi2  25742  bsi3  25744  bsi4  25746  addcanri  25769  issrc  25970  tartarmap  25991  prismorcsetlemc  26020  idcatfun  26044  lemindclsbu  26098  pgapspf  26155  pdiveql  26271  filnetlem3  26432  fdc  26558  ismrer1  26665  reheibor  26666  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  rencldnfi  27007  jm2.27dlem2  27206  wepwso  27242  dfac11  27263  pwssplit4  27294  frlmpwfi  27365  isnumbasgrplem3  27373  mpaaeu  27458  mvdco  27491  proot1mul  27618  proot1hash  27622  seff  27641  sumsnd  27800  stoweidlem34  27886  stoweidlem37  27889  bi123imp0  28560  tendo0co2  31599  erng1r  31806  dvalveclem  31837  dva0g  31839  dvh0g  31923
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator