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  3212  dtru  4628  intasym  5372  relcoi1  5526  funres11  5646  cnvresid  5648  elnn  6695  fparlem1  6885  fparlem2  6886  dftpos4  6976  tposf12  6982  tfr2b  7067  tz7.44lem1  7073  xpcomco  7609  sbthlem2  7630  fidomdm  7804  marypha1lem  7895  hartogslem1  7970  brwdom2  8002  inf3lem6  8053  omex  8063  cantnfvalOLD  8120  cnfcom  8147  cnfcomOLD  8155  cnfcom2OLD  8157  cnfcom3lemOLD  8158  cnfcom3OLD  8159  tz9.1c  8164  r1tr  8197  r1ord3g  8200  rankwflemb  8214  r1elwf  8217  r1elss  8227  rankval3b  8247  onssr1  8252  infxpenlem  8394  alephnbtwn  8455  alephordilem1  8457  alephfp  8492  dfac13  8525  pwsdompw  8587  infcdaabs  8589  ackbij1  8621  ackbij2  8626  r1om  8627  cflim2  8646  fin23lem27  8711  fin23lem29  8724  fin23lem30  8725  fin1a2lem6  8788  fin1a2lem7  8789  fin1a2lem13  8795  itunitc1  8803  itunitc  8804  ituniiun  8805  hsmexlem5  8813  axcc2lem  8819  axcc3  8821  zorn2lem6  8884  zorn2lem7  8885  ttukeylem6  8897  axdc  8904  fodom  8905  iunfo  8917  cardval  8924  cardid  8925  pwcfsdom  8961  alephom  8963  fpwwe  9027  canthp1lem2  9034  canthp1  9035  gchaleph2  9053  r1limwun  9117  inaprc  9217  nqerf  9311  recmulnq  9345  dmrecnq  9349  halfnq  9357  genpdm  9383  reclem3pr  9430  axresscn  9528  axpre-sup  9549  1re  9598  0re  9599  00id  9758  addid1  9763  renegcli  9885  zexALT  10890  uzn0  11106  dfle2  11363  xrinfmss  11511  axdc4uzlem  12073  facnn  12336  fac0  12337  hashgval  12389  hashinf  12391  hashresfn  12394  hashrabrsn  12421  hashrabsn01  12422  hashrabsn1  12423  hashp1i  12449  hashxplem  12472  brfi1uzind  12513  cshw1  12771  cats1fv  12805  cnrecnv  12979  rexanuz  13159  climdm  13358  lo1eq  13372  rlimeq  13373  sumsn  13544  tanval  13844  rpnnen2lem11  13939  rpnnen  13941  sadadd2lem  14090  sadadd3  14092  sadaddlem  14097  sadasslem  14101  sadeq  14103  3prm  14215  unbenlem  14407  prmreclem6  14420  vdwlem8  14487  vdwnnlem1  14494  0ram  14519  structcnvcnv  14624  prdsval  14833  prdsbas  14835  prdsplusg  14836  prdsmulr  14837  prdsvsca  14838  prdshom  14845  xpsfrn  14947  xpsff1o2  14949  catcoppccl  15413  catcfuccl  15414  catcxpccl  15454  tsrss  15831  gsumpropd2lem  15878  symgid  16404  mvdco  16448  efgmnvl  16710  efgval  16713  efgi0  16716  efgi1  16717  efgredeu  16748  0frgp  16775  abln0  16851  lt6abl  16875  gsumval3OLD  16886  gsumval3  16889  gsumzresOLD  16896  gsumzaddOLD  16915  gsum2dlem2  16976  gsum2dOLD  16978  dprdfaddOLD  17045  dprdres  17053  dmdprdsplit2lem  17072  ringn0  17227  isdrng2  17384  drngmcl  17387  drngid2  17390  psrplusg  18012  coe1sfi  18230  coe1sfiOLD  18231  ply1plusgfvi  18261  cnfldplusf  18423  cnfldsub  18424  cnsubmlem  18444  cnmsubglem  18458  gzrngunitlem  18460  rge0srg  18465  zring0  18476  zrng0  18482  mulgghm2OLD  18511  zzngim  18568  zrhpsgnmhm  18597  re0g  18625  pjfval  18714  pjpm  18716  marep01ma  19139  smadiadetlem1a  19142  smadiadetlem3lem2  19146  smadiadetlem3  19147  smadiadetlem4  19148  smadiadet  19149  indistpsALT  19491  tgrest  19637  leordtval2  19690  lmbr2  19737  cnprest  19767  lmff  19779  kgenidm  20025  tx1cn  20087  tx2cn  20088  hausdiag  20123  tsmsresOLD  20622  elrnust  20704  ustbas  20707  ustuqtop0  20720  utopsnneiplem  20727  neipcfilu  20776  psmetge0  20793  xmetge0  20824  qdensere  21254  cnblcld  21259  cnfldms  21260  cnfldtopn  21266  xrsdsre  21292  xrge0tsms  21316  iccpnfcnv  21421  xrhmeo  21423  cnheiborlem  21431  lmmbr2  21675  lmcau  21728  cmetss  21730  cncms  21772  cnfldcusp  21774  ovolctb  21878  ovoliunnul  21895  ismbl  21914  volf  21917  voliunlem1  21937  ioorf  21959  ioorinv  21962  ioorcl  21963  dyaddisj  21982  dyadmax  21984  dyadmbl  21986  mbfid  22020  ismbfd  22024  mbfimaopnlem  22039  limcresi  22266  dvreslem  22290  dvres2lem  22291  dvcjbr  22329  dvferm1  22363  dvferm2  22365  dvlip2  22373  dv11cn  22379  deg1ldg  22469  deg1leb  22472  plycpn  22661  vieta1lem2  22683  elqaa  22694  aalioulem2  22705  aaliou3lem3  22716  aaliou3lem4  22718  pserulm  22793  psercnlem2  22795  psercnlem1  22796  psercn  22797  abelth  22812  reeff1o  22818  pilem1  22822  efhalfpi  22840  coseq0negpitopi  22872  pige3  22886  tanregt0  22902  efif1olem3  22907  efif1olem4  22908  efifo  22910  eff1olem  22911  efsubm  22914  logrn  22922  ellogrn  22923  relogf1o  22930  argregt0  22971  argrege0  22972  dvrelog  22994  dvloglem  23005  logf1o2  23007  dvlog  23008  efopnlem1  23013  efopnlem2  23014  logtayl  23017  cxpcn3lem  23097  cxpcn3  23098  resqrtcn  23099  asinneg  23193  asinrebnd  23208  atan0  23215  atanbnd  23233  areambl  23264  sqrtlim  23278  amgmlem  23295  basellem1  23330  basellem4  23333  sqff1o  23432  dchrplusg  23498  bposlem6  23540  bposlem8  23542  dchrvmasumlem2  23659  mulog2sum  23698  pntibndlem1  23750  pntlemo  23768  qrng0  23782  ostth  23800  lmif  24127  islmib  24129  usgraexmpledg  24379  constr1trl  24566  vdegp1ai  24960  grporn  25190  issubgoi  25288  gidsn  25326  ginvsn  25327  efghgrpOLD  25351  rngomndo  25399  ip0i  25716  ubthlem1  25762  ubthlem2  25763  axhcompl-zf  25891  normlem7  26009  bcseqi  26013  bcsiALT  26072  hlimf  26131  hlimuni  26132  hhshsslem1  26159  hhsssh  26161  hhsscms  26171  occllem  26197  occl  26198  h1deoi  26443  h1dei  26444  h1de2ctlem  26449  h1de2ci  26450  spansni  26451  spanunsni  26473  pjpythi  26616  nmfn0  26882  nmopadjlem  26984  adjcoi  26995  nmopcoadji  26996  pjoccoi  27073  shatomistici  27256  ceqsexv2d  27373  imadifxp  27434  idssxp  27445  xppreima  27463  1stpreima  27500  2ndpreima  27501  dmct  27513  xrge0neqmnf  27656  xrge0tsmsd  27752  reofld  27807  rearchi  27809  nn0archi  27810  xrge0slmod  27811  qtophaus  27816  iistmd  27861  xpinpreima  27865  xpinpreima2  27866  tpr2rico  27871  mndpluscn  27885  xrge0pluscn  27899  cnzh  27928  rezh  27929  qqhucn  27950  rrhcn  27955  cnrrext  27968  zrhre  27974  qqhre  27975  ismntop  27981  sigaex  28086  brsiga  28131  cntnevol  28176  voliune  28178  ddemeas  28185  1stmbfm  28208  2ndmbfm  28209  br2base  28217  dya2icoseg2  28226  dya2iocucvr  28232  eulerpartlemt  28287  eulerpartgbij  28288  eulerpartlemmf  28291  eulerpartlemgvv  28292  eulerpartlemgf  28295  eulerpart  28298  sseqmw  28307  sseqf  28308  sseqp1  28311  fiblem  28314  fibp1  28317  dstrvprob  28387  coinflipspace  28396  coinfliprv  28398  coinflippv  28399  ballotlem1  28402  ballotlem8  28452  lgamucov  28557  iccllyscon  28672  rellyscon  28673  msrid  28882  dfrdg2  29203  omsinds  29274  trpredlem1  29285  trpredtr  29288  trpredmintr  29289  wfrlem14  29331  dfrdg4  29575  imagesset  29578  elhf  29806  limsucncmpi  29885  mblfinlem1  30026  ovoliunnfl  30031  voliunnfl  30033  mbfresfi  30036  dvtanlem  30039  dvtan  30040  itg2addnc  30044  ftc1anclem3  30067  areacirc  30087  filnetlem3  30173  fdc  30213  ismrer1  30309  reheibor  30310  ac6s6f  30556  2rexfrabdioph  30704  3rexfrabdioph  30705  4rexfrabdioph  30706  6rexfrabdioph  30707  7rexfrabdioph  30708  rencldnfi  30730  jm2.27dlem2  30927  wepwso  30963  dfac11  30983  pwssplit4  31010  frlmpwfi  31021  isnumbasgrplem3  31029  mpaaeu  31075  proot1mul  31132  proot1hash  31136  seff  31165  prmunb2  31167  lcmgcdlem  31188  sumsnd  31355  islptre  31533  stoweidlem34  31705  stoweidlem37  31708  stirlinglem11  31755  stirlinglem12  31756  stirlinglem13  31757  fouriersw  31903  2zrng0  32454  lmodn0  32831  zlmodzxzldeplem3  32838  lvecpsslmod  32843  elimhyps  34432  dedths  34433  tendo0co2  36254  erng1r  36461  dvalveclem  36492  dva0g  36494  dvh0g  36578  taupilem3  37434