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 5 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 5 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  eqvinc  3065  elnn  4858  intasym  5252  relcoi1  5401  funres11  5524  cnvresid  5526  fparlem1  6449  fparlem2  6450  dftpos4  6501  tposf12  6507  tfr2b  6660  tz7.44lem1  6666  xpcomco  7201  sbthlem2  7221  fidomdm  7391  marypha1lem  7441  hartogslem1  7514  brwdom2  7544  inf3lem6  7591  omex  7601  cantnfdm  7622  cantnfval  7626  cantnff  7632  cnfcom  7660  cnfcom2  7662  cnfcom3lem  7663  cnfcom3  7664  tz9.1c  7669  r1tr  7705  r1ord3g  7708  rankwflemb  7722  r1elwf  7725  r1elss  7735  rankval3b  7755  onssr1  7760  infxpenlem  7900  alephnbtwn  7957  alephordilem1  7959  alephfp  7994  dfac13  8027  pwsdompw  8089  infcdaabs  8091  ackbij1  8123  ackbij2  8128  r1om  8129  cflim2  8148  fin23lem27  8213  fin23lem29  8226  fin23lem30  8227  fin1a2lem6  8290  fin1a2lem7  8291  fin1a2lem13  8297  itunitc1  8305  itunitc  8306  ituniiun  8307  hsmexlem5  8315  axcc2lem  8321  axcc3  8323  zorn2lem6  8386  zorn2lem7  8387  ttukeylem6  8399  axdc  8406  fodom  8407  iunfo  8419  cardval  8426  cardid  8427  pwcfsdom  8463  alephom  8465  fpwwe  8526  canthp1lem2  8533  canthp1  8534  gchaleph2  8552  r1limwun  8616  inaprc  8716  nqerf  8812  recmulnq  8846  dmrecnq  8850  halfnq  8858  genpdm  8884  reclem3pr  8931  axresscn  9028  axpre-sup  9049  1re  9095  0re  9096  00id  9246  addid1  9251  renegcli  9367  zexALT  10305  uzn0  10506  dfle2  10745  xrinfmss  10893  axdc4uzlem  11326  facnn  11573  fac0  11574  hashgval  11626  hashinf  11628  hashrabrsn  11653  hashp1i  11677  hashxplem  11701  brfi1uzind  11720  cats1fv  11828  cnrecnv  11975  rexanuz  12154  climdm  12353  lo1eq  12367  rlimeq  12368  sumsn  12539  tanval  12734  rpnnen2lem11  12829  rpnnen  12831  sadadd2lem  12976  sadadd3  12978  sadaddlem  12983  sadasslem  12987  sadeq  12989  3prm  13101  unbenlem  13281  prmreclem6  13294  vdwlem8  13361  vdwnnlem1  13368  0ram  13393  structcnvcnv  13485  prdsval  13683  prdsbas  13685  prdsplusg  13686  prdsmulr  13687  prdsvsca  13688  prdshom  13694  xpsfrn  13799  xpsff1o2  13801  catcoppccl  14268  catcfuccl  14269  catcxpccl  14309  tsrss  14660  symgid  15109  efgmnvl  15351  efgval  15354  efgi0  15357  efgi1  15358  efgredeu  15389  0frgp  15416  lt6abl  15509  gsumval3  15519  gsumzres  15522  gsumzadd  15532  gsum2d  15551  dprdfadd  15583  dprdres  15591  dmdprdsplit2lem  15608  isdrng2  15850  drngmcl  15853  drngid2  15856  psrplusg  16450  coe1sfi  16615  ply1plusgfvi  16641  cnfldplusf  16733  cnfldsub  16734  cnsubmlem  16751  cnmsubglem  16766  gzrngunitlem  16768  mulgghm2  16791  zzngim  16838  pjfval  16938  pjpm  16940  indistpsALT  17082  tgrest  17228  leordtval2  17281  lmbr2  17328  cnprest  17358  lmff  17370  kgenidm  17584  tx1cn  17646  tx2cn  17647  hausdiag  17682  tsmsres  18178  elrnust  18259  ustbas  18262  ustuqtop0  18275  utopsnneiplem  18282  neipcfilu  18331  psmetge0  18348  xmetge0  18379  qdensere  18809  cnblcld  18814  cnfldms  18815  cnfldtopn  18821  xrsdsre  18846  xrge0tsms  18870  iccpnfcnv  18974  xrhmeo  18976  cnheiborlem  18984  lmmbr2  19217  lmcau  19270  cmetss  19272  cncms  19314  cnfldcusp  19316  ovolctb  19391  ovoliunnul  19408  ismbl  19427  volf  19430  voliunlem1  19449  ioorf  19470  ioorinv  19473  ioorcl  19474  dyaddisj  19493  dyadmax  19495  dyadmbl  19497  mbfid  19531  ismbfd  19535  mbfimaopnlem  19550  limcresi  19777  dvreslem  19801  dvres2lem  19802  dvcjbr  19840  dvferm1  19874  dvferm2  19876  dvlip2  19884  dv11cn  19890  tdeglem4  19988  deg1ldg  20020  deg1leb  20023  plycpn  20211  vieta1lem2  20233  elqaa  20244  aalioulem2  20255  aaliou3lem3  20266  aaliou3lem4  20268  pserulm  20343  psercnlem2  20345  psercnlem1  20346  psercn  20347  abelth  20362  reeff1o  20368  pilem1  20372  efhalfpi  20384  coseq0negpitopi  20416  pige3  20430  tanregt0  20446  efif1olem3  20451  efif1olem4  20452  efifo  20454  eff1olem  20455  logrn  20461  ellogrn  20462  relogf1o  20469  argregt0  20510  argrege0  20511  dvrelog  20533  dvloglem  20544  logf1o2  20546  dvlog  20547  efopnlem1  20552  efopnlem2  20553  logtayl  20556  cxpcn3lem  20636  cxpcn3  20637  resqrcn  20638  asinneg  20731  asinrebnd  20746  atan0  20753  atanbnd  20771  areambl  20802  sqrlim  20816  amgmlem  20833  basellem1  20868  basellem4  20871  sqff1o  20970  dchrplusg  21036  bposlem6  21078  bposlem8  21080  lgseisenlem4  21141  dchrvmasumlem2  21197  dchrisum0flblem1  21207  mulog2sum  21236  pntibndlem1  21288  pntlemo  21306  qrng0  21320  ostth  21338  constr1trl  21593  vdegp1ai  21711  grporn  21805  issubgoi  21903  gidsn  21941  ginvsn  21942  rngomndo  22014  ip0i  22331  ubthlem1  22377  ubthlem2  22378  axhcompl-zf  22506  normlem7  22623  bcseqi  22627  bcsiALT  22686  hlimf  22745  hlimuni  22746  hhshsslem1  22772  hhsssh  22774  hhsscms  22784  occllem  22810  occl  22811  h1deoi  23056  h1dei  23057  h1de2ctlem  23062  h1de2ci  23063  spansni  23064  spanunsni  23086  pjpythi  23229  nmfn0  23495  nmopadjlem  23597  adjcoi  23608  nmopcoadji  23609  pjoccoi  23686  shatomistici  23869  ceqsexv2d  23990  imadifxp  24043  xppreima  24064  1stpreima  24100  2ndpreima  24101  dmct  24111  hashresfn  24161  xrge0neqmnf  24217  gsumpropd2lem  24225  xrge0tsmsd  24228  zzs0  24272  re0g  24278  iistmd  24305  xpinpreima  24309  xpinpreima2  24310  tpr2rico  24315  mndpluscn  24317  xrge0pluscn  24331  cnzh  24359  rezh  24360  zrhre  24390  qqhre  24391  rrhre  24392  sigaex  24497  brsiga  24542  cntnevol  24587  voliune  24590  1stmbfm  24615  2ndmbfm  24616  br2base  24624  dya2iocucvr  24639  dstrvprob  24734  coinflipspace  24743  coinfliprv  24745  coinflippv  24746  ballotlem1  24749  ballotlem8  24799  lgamucov  24827  iccllyscon  24942  rellyscon  24943  dfrdg2  25428  omsinds  25499  trpredlem1  25510  trpredtr  25513  trpredmintr  25514  wfrlem14  25556  dfrdg4  25800  imagesset  25803  elhf  26120  limsucncmpi  26200  ovoliunnfl  26260  voliunnfl  26262  mbfresfi  26265  dvtanlem  26268  dvtan  26269  itg2addnc  26273  ftc1anclem3  26296  areacirc  26311  filnetlem3  26423  fdc  26463  ismrer1  26561  reheibor  26562  2rexfrabdioph  26870  3rexfrabdioph  26871  4rexfrabdioph  26872  6rexfrabdioph  26873  7rexfrabdioph  26874  rencldnfi  26896  jm2.27dlem2  27095  wepwso  27131  dfac11  27151  pwssplit4  27182  frlmpwfi  27253  isnumbasgrplem3  27261  mpaaeu  27346  mvdco  27379  proot1mul  27506  proot1hash  27510  seff  27529  sumsnd  27687  stoweidlem34  27773  stoweidlem37  27776  stirlinglem11  27823  stirlinglem12  27824  cshw1  28309  tendo0co2  31659  erng1r  31866  dvalveclem  31897  dva0g  31899  dvh0g  31983
This theorem was proved from axioms:  ax-mp 5
  Copyright terms: Public domain W3C validator