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 5	. 2 |- ps
4		mp2b.3	. 2 |- ( ps -> ch )
5	3, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  eqvinc  3195  dtru  4608  intasym  5227  relcoi1OLD  5377  funres11  5661  cnvresid  5663  elnn  6708  omsinds  6717  fparlem1  6899  fparlem2  6900  dftpos4  6992  tposf12  6998  wfrlem14  7049  tfr2b  7114  tz7.44lem1  7123  xpcomco  7660  sbthlem2  7681  fidomdm  7851  marypha1lem  7945  hartogslem1  8055  brwdom2  8086  inf3lem6  8136  omex  8146  cnfcom  8202  tz9.1c  8211  r1tr  8244  r1ord3g  8247  rankwflemb  8261  r1elwf  8264  r1elss  8274  rankval3b  8294  onssr1  8299  infxpenlem  8441  alephnbtwn  8498  alephordilem1  8500  alephfp  8535  dfac13  8568  pwsdompw  8630  infcdaabs  8632  ackbij1  8664  ackbij2  8669  r1om  8670  cflim2  8689  fin23lem27  8754  fin23lem29  8767  fin23lem30  8768  fin1a2lem6  8831  fin1a2lem7  8832  fin1a2lem13  8838  itunitc1  8846  itunitc  8847  ituniiun  8848  hsmexlem5  8856  axcc2lem  8862  axcc3  8864  zorn2lem6  8927  zorn2lem7  8928  ttukeylem6  8940  axdc  8947  fodom  8948  iunfo  8960  cardval  8967  cardid  8968  pwcfsdom  9004  alephom  9006  fpwwe  9067  canthp1lem2  9074  canthp1  9075  gchaleph2  9093  r1limwun  9157  inaprc  9257  nqerf  9351  recmulnq  9385  dmrecnq  9389  halfnq  9397  genpdm  9423  reclem3pr  9470  axresscn  9568  axpre-sup  9589  1re  9638  0re  9639  00id  9804  addid1  9809  renegcli  9931  zexALT  10952  uzn0  11170  dfle2  11442  xrinfmss  11591  axdc4uzlem  12188  facnn  12454  fac0  12455  hashgval  12511  hashinf  12513  hashresfn  12516  hashrabrsn  12544  hashrabsn01  12545  hashrabsn1  12546  hashp1i  12573  hashxplem  12596  brfi1uzind  12637  cshw1  12902  cats1fv  12936  trclubgi  13040  cnrecnv  13207  rexanuz  13387  climdm  13596  lo1eq  13610  rlimeq  13611  sumsn  13785  tanval  14160  rpnnen2lem11  14255  rpnnen  14257  sadadd2lem  14411  sadadd3  14413  sadaddlem  14418  sadasslem  14422  sadeq  14424  lcmgcdlem  14549  3prm  14619  unbenlem  14830  prmreclem6  14843  vdwlem8  14916  vdwnnlem1  14923  0ram  14956  prmgaplcmlem1OLD  14990  prmgaplcmlem2OLD  14991  prmdvdsprmorpOLD  14994  prmgapprmorlemOLD  14995  prmorlelcmfOLD  14998  prmorlelcmsOLDOLD  15000  structcnvcnv  15110  prdsval  15331  prdsbas  15333  prdsplusg  15334  prdsmulr  15335  prdsvsca  15336  prdshom  15343  xpsfrn  15453  xpsff1o2  15455  catcoppccl  15981  catcfuccl  15982  catcxpccl  16070  tsrss  16447  gsumpropd2lem  16494  symgid  17020  mvdco  17064  efgmnvl  17342  efgval  17345  efgi0  17348  efgi1  17349  efgredeu  17380  0frgp  17407  abln0  17483  lt6abl  17507  gsumval3  17519  gsum2dlem2  17581  dprdres  17639  dmdprdsplit2lem  17656  ringn0  17809  isdrng2  17963  drngmcl  17966  drngid2  17969  psrplusg  18583  coe1sfi  18784  ply1plusgfvi  18813  cnfldplusf  18973  cnfldsub  18974  cnsubmlem  18994  cnmsubglem  19008  gzrngunitlem  19010  rge0srg  19015  zring0  19026  zzngim  19100  zrhpsgnmhm  19129  re0g  19157  pjfval  19246  pjpm  19248  marep01ma  19662  smadiadetlem1a  19665  smadiadetlem3lem2  19669  smadiadetlem3  19670  smadiadetlem4  19671  smadiadet  19672  indistpsALT  20005  tgrest  20152  leordtval2  20205  lmbr2  20252  cnprest  20282  lmff  20294  kgenidm  20539  tx1cn  20601  tx2cn  20602  hausdiag  20637  elrnust  21216  ustbas  21219  ustuqtop0  21232  utopsnneiplem  21239  neipcfilu  21288  psmetge0  21305  xmetge0  21336  qdensere  21767  cnblcld  21772  cnfldms  21773  cnfldtopn  21779  xrsdsre  21805  xrge0tsms  21829  iccpnfcnv  21949  xrhmeo  21951  cnheiborlem  21959  lmmbr2  22206  lmcau  22259  cmetss  22261  cncms  22299  cnfldcusp  22301  ovolctb  22420  ovoliunnul  22437  ismbl  22457  volf  22460  voliunlem1  22480  ioorf  22502  ioorinv  22505  ioorcl  22506  ioorfOLD  22507  ioorinvOLD  22510  ioorclOLD  22511  dyaddisj  22531  dyadmax  22533  dyadmbl  22535  mbfid  22569  ismbfd  22573  mbfimaopnlem  22588  limcresi  22817  dvreslem  22841  dvres2lem  22842  dvcjbr  22880  dvferm1  22914  dvferm2  22916  dvlip2  22924  dv11cn  22930  deg1ldg  23018  deg1leb  23021  plycpn  23219  vieta1lem2  23241  elqaa  23255  aalioulem2  23266  aaliou3lem3  23277  aaliou3lem4  23279  pserulm  23354  psercnlem2  23356  psercnlem1  23357  psercn  23358  abelth  23373  reeff1o  23379  pilem1  23383  efhalfpi  23403  coseq0negpitopi  23435  pige3  23449  tanregt0  23465  efif1olem3  23470  efif1olem4  23471  efifo  23473  eff1olem  23474  efsubm  23477  logrn  23485  ellogrn  23486  relogf1o  23493  argregt0  23536  argrege0  23537  dvrelog  23559  dvloglem  23570  logf1o2  23572  dvlog  23573  efopnlem1  23578  efopnlem2  23579  logtayl  23582  cxpcn3lem  23664  cxpcn3  23665  resqrtcn  23666  asinneg  23789  asinrebnd  23804  atan0  23811  atanbnd  23829  areambl  23861  sqrtlim  23875  amgmlem  23892  lgamucov  23940  basellem1  23984  basellem4  23987  sqff1o  24086  dchrplusg  24152  bposlem6  24194  bposlem8  24196  dchrvmasumlem2  24313  mulog2sum  24352  pntibndlem1  24404  pntlemo  24422  qrng0  24436  ostth  24454  lmif  24804  islmib  24806  usgraexmpledg  25107  constr1trl  25294  vdegp1ai  25688  grporn  25916  issubgoi  26014  gidsn  26052  ginvsn  26053  efghgrpOLD  26077  rngomndo  26125  ip0i  26442  ubthlem1  26488  ubthlem2  26489  axhcompl-zf  26627  normlem7  26745  bcseqi  26749  bcsiALT  26808  hlimf  26866  hlimuni  26867  hhshsslem1  26894  hhsssh  26896  hhsscms  26906  occllem  26932  occl  26933  h1deoi  27178  h1dei  27179  h1de2ctlem  27184  h1de2ci  27185  spansni  27186  spanunsni  27208  pjpythi  27351  nmfn0  27616  nmopadjlem  27718  adjcoi  27729  nmopcoadji  27730  pjoccoi  27807  shatomistici  27990  ceqsexv2d  28110  imadifxp  28192  idssxp  28208  xppreima  28229  1stpreima  28268  2ndpreima  28269  dmct  28283  xrge0neqmnf  28440  gsummpt2d  28532  xrge0tsmsd  28537  reofld  28592  rearchi  28594  nn0archi  28595  xrge0slmod  28596  qtophaus  28652  iistmd  28697  xpinpreima  28701  xpinpreima2  28702  tpr2rico  28707  mndpluscn  28721  xrge0pluscn  28735  cnzh  28763  rezh  28764  qqhucn  28785  rrhcn  28790  cnrrext  28803  zrhre  28812  qqhre  28813  ismntop  28819  sigaex  28920  brsiga  28994  cntnevol  29039  voliune  29041  ddemeas  29048  1stmbfm  29071  2ndmbfm  29072  br2base  29080  dya2icoseg2  29089  dya2iocucvr  29095  carsgclctunlem2  29140  carsgclctunlem3  29141  sitgaddlemb  29170  eulerpartlemt  29193  eulerpartgbij  29194  eulerpartlemmf  29197  eulerpartlemgvv  29198  eulerpartlemgf  29201  eulerpart  29204  sseqmw  29213  sseqf  29214  sseqp1  29217  fiblem  29220  fibp1  29223  dstrvprob  29293  coinflipspace  29302  coinfliprv  29304  coinflippv  29305  ballotlem1  29308  ballotlem8  29358  ballotlem8OLD  29396  iccllyscon  29962  rellyscon  29963  msrid  30172  dfrdg2  30430  trpredlem1  30456  trpredtr  30459  trpredmintr  30460  dfrdg4  30704  imagesset  30706  elhf  30927  filnetlem3  31022  limsucncmpi  31091  taupilem3  31666  icoreresf  31690  icoreelrnab  31692  relowlssretop  31701  poimirlem3  31851  poimirlem9  31857  poimirlem15  31863  poimirlem16  31864  poimirlem17  31865  poimirlem19  31867  poimirlem27  31875  poimirlem28  31876  poimirlem31  31879  poimirlem32  31880  mblfinlem1  31885  ovoliunnfl  31890  voliunnfl  31892  mbfresfi  31895  dvtanlemOLD  31899  dvtan  31900  itg2addnc  31904  ftc1anclem3  31927  areacirc  31945  fdc  31982  ismrer1  32078  reheibor  32079  ac6s6f  32324  elimhyps  32446  dedths  32447  tendo0co2  34268  erng1r  34475  dvalveclem  34506  dva0g  34508  dvh0g  34592  2rexfrabdioph  35552  3rexfrabdioph  35553  4rexfrabdioph  35554  6rexfrabdioph  35555  7rexfrabdioph  35556  rencldnfi  35577  jm2.27dlem2  35779  wepwso  35815  dfac11  35834  pwssplit4  35861  frlmpwfi  35870  isnumbasgrplem3  35878  mpaaeu  35930  proot1mul  35987  proot1hash  35991  frege92  36403  seff  36509  prmunb2  36511  binomcxplemdvbinom  36554  binomcxplemcvg  36555  binomcxplemnotnn0  36557  sumsnd  37202  sumsnf  37438  islptre  37486  stoweidlem34  37682  stoweidlem37  37685  stirlinglem11  37733  stirlinglem12  37734  stirlinglem13  37735  fouriersw  37882  gboge7  38484  nnsum3primes4  38503  structiedg0val  38691  snstriedgval  38697  2zrng0  39000  lmodn0  39352  zlmodzxzldeplem3  39359  lvecpsslmod  39364  0dig2pr01  39486  aacllem  39605