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

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 |- ph
2		mp2b.2	. . 3 |- ( ph -> ps )
3	1, 2	ax-mp 8	. 2 |- ps
4		mp2b.3	. 2 |- ( ps -> ch )
5	3, 4	ax-mp 8	1 |- ch

Syntax hints:   -> wi 4

This theorem is referenced by:  eqvinc  3023  elnn  4814  intasym  5208  relcoi1  5357  funres11  5480  cnvresid  5482  fparlem1  6405  fparlem2  6406  dftpos4  6457  tposf12  6463  tfr2b  6616  tz7.44lem1  6622  xpcomco  7157  sbthlem2  7177  fidomdm  7347  marypha1lem  7396  hartogslem1  7467  brwdom2  7497  inf3lem6  7544  omex  7554  cantnfdm  7575  cantnfval  7579  cantnff  7585  cnfcom  7613  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  tz9.1c  7622  r1tr  7658  r1ord3g  7661  rankwflemb  7675  r1elwf  7678  r1elss  7688  rankval3b  7708  onssr1  7713  infxpenlem  7851  alephnbtwn  7908  alephordilem1  7910  alephfp  7945  dfac13  7978  pwsdompw  8040  infcdaabs  8042  ackbij1  8074  ackbij2  8079  r1om  8080  cflim2  8099  fin23lem27  8164  fin23lem29  8177  fin23lem30  8178  fin1a2lem6  8241  fin1a2lem7  8242  fin1a2lem13  8248  itunitc1  8256  itunitc  8257  ituniiun  8258  hsmexlem5  8266  axcc2lem  8272  axcc3  8274  zorn2lem6  8337  zorn2lem7  8338  ttukeylem6  8350  axdc  8357  fodom  8358  iunfo  8370  cardval  8377  cardid  8378  pwcfsdom  8414  alephom  8416  fpwwe  8477  canthp1lem2  8484  canthp1  8485  gchaleph2  8507  r1limwun  8567  inaprc  8667  nqerf  8763  recmulnq  8797  dmrecnq  8801  halfnq  8809  genpdm  8835  reclem3pr  8882  axresscn  8979  axpre-sup  9000  1re  9046  0re  9047  00id  9197  addid1  9202  renegcli  9318  zexALT  10256  uzn0  10457  dfle2  10696  xrinfmss  10844  axdc4uzlem  11276  facnn  11523  fac0  11524  hashgval  11576  hashinf  11578  hashrabrsn  11603  hashp1i  11627  hashxplem  11651  brfi1uzind  11670  cats1fv  11778  cnrecnv  11925  rexanuz  12104  climdm  12303  lo1eq  12317  rlimeq  12318  sumsn  12489  tanval  12684  rpnnen2lem11  12779  rpnnen  12781  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  3prm  13051  unbenlem  13231  prmreclem6  13244  vdwlem8  13311  vdwnnlem1  13318  0ram  13343  structcnvcnv  13435  prdsval  13633  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdshom  13644  xpsfrn  13749  xpsff1o2  13751  catcoppccl  14218  catcfuccl  14219  catcxpccl  14259  tsrss  14610  symgid  15059  efgmnvl  15301  efgval  15304  efgi0  15307  efgi1  15308  efgredeu  15339  0frgp  15366  lt6abl  15459  gsumval3  15469  gsumzres  15472  gsumzadd  15482  gsum2d  15501  dprdfadd  15533  dprdres  15541  dmdprdsplit2lem  15558  isdrng2  15800  drngmcl  15803  drngid2  15806  psrplusg  16400  coe1sfi  16565  ply1plusgfvi  16591  cnfldplusf  16683  cnfldsub  16684  cnsubmlem  16701  cnmsubglem  16716  gzrngunitlem  16718  mulgghm2  16741  zzngim  16788  pjfval  16888  pjpm  16890  indistpsALT  17032  tgrest  17177  leordtval2  17230  lmbr2  17277  cnprest  17307  lmff  17319  kgenidm  17532  tx1cn  17594  tx2cn  17595  hausdiag  17630  tsmsres  18126  elrnust  18207  ustbas  18210  ustuqtop0  18223  utopsnneiplem  18230  neipcfilu  18279  psmetge0  18296  xmetge0  18327  qdensere  18757  cnblcld  18762  cnfldms  18763  cnfldtopn  18769  xrsdsre  18794  xrge0tsms  18818  iccpnfcnv  18922  xrhmeo  18924  cnheiborlem  18932  lmmbr2  19165  lmcau  19218  cmetss  19220  cncms  19262  cnfldcusp  19264  ovolctb  19339  ovoliunnul  19356  ismbl  19375  volf  19378  voliunlem1  19397  ioorf  19418  ioorinv  19421  ioorcl  19422  dyaddisj  19441  dyadmax  19443  dyadmbl  19445  mbfid  19481  ismbfd  19485  mbfimaopnlem  19500  limcresi  19725  dvreslem  19749  dvres2lem  19750  dvcjbr  19788  dvferm1  19822  dvferm2  19824  dvlip2  19832  dv11cn  19838  tdeglem4  19936  deg1ldg  19968  deg1leb  19971  plycpn  20159  vieta1lem2  20181  elqaa  20192  aalioulem2  20203  aaliou3lem3  20214  aaliou3lem4  20216  pserulm  20291  psercnlem2  20293  psercnlem1  20294  psercn  20295  abelth  20310  reeff1o  20316  pilem1  20320  efhalfpi  20332  coseq0negpitopi  20364  pige3  20378  tanregt0  20394  efif1olem3  20399  efif1olem4  20400  efifo  20402  eff1olem  20403  logrn  20409  ellogrn  20410  relogf1o  20417  argregt0  20458  argrege0  20459  dvrelog  20481  dvloglem  20492  logf1o2  20494  dvlog  20495  efopnlem1  20500  efopnlem2  20501  logtayl  20504  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  asinneg  20679  asinrebnd  20694  atan0  20701  atanbnd  20719  areambl  20750  sqrlim  20764  amgmlem  20781  basellem1  20816  basellem4  20819  sqff1o  20918  dchrplusg  20984  bposlem6  21026  bposlem8  21028  lgseisenlem4  21089  dchrvmasumlem2  21145  dchrisum0flblem1  21155  mulog2sum  21184  pntibndlem1  21236  pntlemo  21254  qrng0  21268  ostth  21286  constr1trl  21541  vdegp1ai  21659  grporn  21753  issubgoi  21851  gidsn  21889  ginvsn  21890  rngomndo  21962  ip0i  22279  ubthlem1  22325  ubthlem2  22326  axhcompl-zf  22454  normlem7  22571  bcseqi  22575  bcsiALT  22634  hlimf  22693  hlimuni  22694  hhshsslem1  22720  hhsssh  22722  hhsscms  22732  occllem  22758  occl  22759  h1deoi  23004  h1dei  23005  h1de2ctlem  23010  h1de2ci  23011  spansni  23012  spanunsni  23034  pjpythi  23177  nmfn0  23443  nmopadjlem  23545  adjcoi  23556  nmopcoadji  23557  pjoccoi  23634  shatomistici  23817  ceqsexv2d  23938  imadifxp  23991  xppreima  24012  1stpreima  24048  2ndpreima  24049  dmct  24059  hashresfn  24109  xrge0neqmnf  24165  gsumpropd2lem  24173  xrge0tsmsd  24176  zzs0  24220  re0g  24226  iistmd  24253  xpinpreima  24257  xpinpreima2  24258  tpr2rico  24263  mndpluscn  24265  xrge0pluscn  24279  cnzh  24307  rezh  24308  zrhre  24338  qqhre  24339  rrhre  24340  sigaex  24445  brsiga  24490  cntnevol  24535  voliune  24538  1stmbfm  24563  2ndmbfm  24564  br2base  24572  dya2iocucvr  24587  dstrvprob  24682  coinflipspace  24691  coinfliprv  24693  coinflippv  24694  ballotlem1  24697  ballotlem8  24747  lgamucov  24775  iccllyscon  24890  rellyscon  24891  dfrdg2  25366  omsinds  25433  trpredlem1  25444  trpredtr  25447  trpredmintr  25448  wfrlem14  25483  dfrdg4  25703  elhf  26019  limsucncmpi  26099  ovoliunnfl  26147  voliunnfl  26149  mbfresfi  26152  itg2addnc  26158  areacirc  26187  filnetlem3  26299  fdc  26339  ismrer1  26437  reheibor  26438  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  rencldnfi  26772  jm2.27dlem2  26971  wepwso  27007  dfac11  27028  pwssplit4  27059  frlmpwfi  27130  isnumbasgrplem3  27138  mpaaeu  27223  mvdco  27256  proot1mul  27383  proot1hash  27387  seff  27406  sumsnd  27564  stoweidlem34  27650  stoweidlem37  27653  stirlinglem11  27700  stirlinglem12  27701  tendo0co2  31270  erng1r  31477  dvalveclem  31508  dva0g  31510  dvh0g  31594

This theorem was proved from axioms:  ax-mp 8