Theorem mp2b 10

Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)

Hypotheses

Ref	Expression
mp2b.1	⊢ 𝜑
mp2b.2	⊢ (𝜑 → 𝜓)
mp2b.3	⊢ (𝜓 → 𝜒)

Assertion

Ref	Expression
mp2b	⊢ 𝜒

Proof of Theorem mp2b

Step	Hyp	Ref	Expression
1		mp2b.1	. . 3 ⊢ 𝜑
2		mp2b.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4		mp2b.3	. 2 ⊢ (𝜓 → 𝜒)
5	3, 4	ax-mp 5	1 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  minimp-syllsimp  1655  dtruALT2  5336  intasym  6121  relcoi2  6298  funres11  6639  cnvresidOLD  6641  find  7931  fparlem1  8150  fparlem2  8151  dftpos4  8290  tposf12  8296  tfr2b  8432  tz7.44lem1  8441  ord3  8520  xp01disjl  8528  on2recsfn  8704  on2recsov  8705  on2ind  8706  on3ind  8707  xpcomco  9114  sbthlem2  9135  fidomdm  9351  brwdom2  9594  epnsym  9637  inf3lem6  9661  cnfcom  9728  ttrclco  9746  ttrclselem2  9754  tz9.1c  9758  frr1  9790  r1tr  9810  r1ord3g  9813  rankwflembOLD  9828  r1elwf  9831  r1elss  9841  rankval3b  9863  onssr1  9870  elhfOLD  9935  inlresf  10022  inrresf  10024  djuin  10026  infxpenlem  10119  alephnbtwn  10177  alephordilem1  10179  alephfp  10214  dfac13  10248  pwsdompw  10308  infdjuabs  10310  ackbij1  10342  ackbij2  10347  cflim2  10368  fin23lem27  10433  fin23lem29  10446  fin23lem30  10447  fin1a2lem6  10510  fin1a2lem7  10511  fin1a2lem13  10517  itunitc1  10525  itunitc  10526  ituniiun  10527  hsmexlem5  10535  axcc2lem  10541  axcc3  10543  zorn2lem6  10606  zorn2lem7  10607  ttukeylem6  10619  dmct  10629  dmctOLD  10630  iunfo  10650  cardval  10657  cardid  10658  alephom  10697  canthp1lem2  10765  gchaleph2  10784  r1limwun  10848  inaprc  10948  nqerf  11042  recmulnq  11076  dmrecnq  11080  halfnq  11088  genpdm  11114  reclem3pr  11161  axresscn  11260  axpre-sup  11281  1re  11335  0re  11337  00id  11512  addrid  11517  0cnALT  11572  renegcli  11646  zexALT  12740  uzn0  13009  xrinfmss  13467  axdc4uzlem  14153  facnn  14446  fac0  14447  hashgval  14504  hashinf  14506  hashresfn  14511  hashrabrsn  14543  hashrabsn01  14544  hashrabsn1  14545  hashp1i  14574  hash1snb  14591  hashxplem  14605  fi1uzind  14679  cshw1  15001  cats1fv  15038  s7f1o  15148  trclubgi  15179  cnrecnv  15361  rexanuz  15542  climdm  15750  lo1eq  15764  rlimeq  15765  sumsnf  15938  tanval  16325  rpnnen2lem11  16421  rpnnen  16424  sadadd2lem  16658  sadadd3  16660  sadaddlem  16665  sadasslem  16669  sadeq  16671  lcmgcdlem  16810  unbenlem  17115  prmreclem6  17128  vdwlem8  17195  vdwnnlem1  17202  0ram  17227  structcnvcnv  17360  prdsvallem  17654  prdsval  17655  prdsbas  17657  prdsplusg  17658  prdsmulr  17659  prdsvsca  17660  prdshom  17667  xpsfrn  17769  xpsff1o2  17770  catcoppccl  18321  catcfuccl  18322  catcxpccl  18410  tsrss  18792  gsumpropd2lem  18897  smndex2dnrinv  19143  mvdco  19689  efgmnvl  19958  efgval  19961  efgi0  19964  efgi1  19965  efgredeu  19996  0frgp  20023  abln0  20111  lt6abl  20139  gsumval3  20151  gsum2dlem2  20215  dprdres  20274  dmdprdsplit2lem  20291  ringn0  20572  isdrng2  21027  drngid2  21040  cnfldplusf  21735  cnfldsub  21736  cnsubmlem  21751  cnsubglem  21752  cnmsubglem  21766  gzrngunitlem  21768  rge0srg  21774  zring0  21794  pzriprnglem10  21826  zzngim  21888  zrhpsgnmhm  21920  re0g  21948  pjfval  22042  pjpm  22044  psrplusg  22275  coe1sfi  22561  ply1plusgfvi  22589  marep01ma  23005  smadiadetlem1a  23008  smadiadetlem3lem2  23012  smadiadetlem3  23013  smadiadetlem4  23014  smadiadet  23015  indistpsALT  23361  tgrest  23507  leordtval2  23560  lmbr2  23607  cnprest  23637  lmff  23649  kgenidm  23896  tx1cn  23958  tx2cn  23959  ustbas  24576  psmetge0  24661  xmetge0  24693  qdensere  25118  cnblcld  25123  cnfldms  25124  cnfldtopn  25130  xrsdsre  25160  xrge0tsms  25184  iccpnfcnv  25295  xrhmeo  25297  cnheiborlem  25305  cnlmod  25491  recvs  25497  lmmbr2  25610  lmcau  25664  metsscmetcld  25666  cncms  25706  cnfldcusp  25708  ovolctb  25841  ovoliunnul  25858  ismbl  25877  volf  25880  voliunlem1  25901  ioorf  25924  ioorinv  25927  ioorcl  25928  dyaddisj  25947  dyadmax  25949  dyadmbl  25951  mbfid  25986  ismbfd  25990  mbfimaopnlem  26006  limcresi  26235  dvreslem  26259  dvres2lem  26260  dvcjbr  26299  dvferm1  26335  dvferm2  26337  dvlip2  26345  dv11cn  26351  deg1ldg  26440  deg1leb  26443  plycpn  26640  vieta1lem2  26664  elqaa  26675  aalioulem2  26690  aaliou3lem3  26701  aaliou3lem4  26703  pserulm  26779  psercnlem2  26781  psercnlem1  26782  psercn  26783  abelth  26798  reeff1o  26804  pilem1  26808  efhalfpi  26830  coseq0negpitopi  26862  pige3ALT  26878  tanregt0  26897  efif1olem3  26902  efif1olem4  26903  efifo  26905  eff1olem  26906  efsubm  26909  logrn  26916  ellogrn  26917  relogf1o  26924  argregt0  26968  argrege0  26969  dvrelog  26995  dvloglem  27006  logf1o2  27008  dvlog  27009  efopnlem1  27014  efopnlem2  27015  logtayl  27018  cxpcn3lem  27105  cxpcn3  27106  resqrtcn  27107  asinneg  27244  asinrebnd  27259  atan0  27266  atanbnd  27284  areambl  27316  sqrtlim  27330  amgmlem  27347  lgamucov  27395  basellem1  27438  basellem4  27441  sqff1o  27539  dchrplusg  27604  bposlem6  27646  bposlem8  27648  dchrvmasumlem2  27855  pntibndlem1  27946  pntlemo  27964  qrng0  27978  ostth  27996  noextendseq  28054  bday0  28227  oldlim  28303  ons2ind  28691  zsex  28796  lmif  29320  islmib  29322  structiedg0val  29630  snstriedgval  29646  umgredgnlp  29755  usgrexmplef  29870  usgrexmpledg  29873  vtxdlfgrval  30096  upgr2pthnlp  30348  konigsberglem5  30887  ex-mod  31080  nowisdomv  31105  pliguhgr  31118  grporn  31153  ip0i  31457  ubthlem1  31502  ubthlem2  31503  axhcompl-zf  31630  normlem7  31748  bcseqi  31752  bcsiALT  31811  hlimf  31869  hlimuni  31870  hhssabloilem  31893  hhshsslem1  31899  hhsssh  31901  hhsscms  31910  occllem  31935  occl  31936  h1deoi  32181  h1dei  32182  h1de2ctlem  32187  h1de2ci  32188  spansni  32189  spanunsni  32211  pjpythi  32354  nmfn0  32619  nmopadjlem  32721  adjcoi  32732  nmopcoadji  32733  pjoccoi  32810  shatomistici  32993  iuninc  33227  imadifxp  33267  xppreima  33311  1stpreima  33371  2ndpreima  33372  fsuppcurry1  33386  fsuppcurry2  33387  hashgt1  33470  s3clhash  33582  gsummpt2d  33680  xrge0tsmsd  33704  tocyc01  33749  cyc3evpm  33781  cycpmconjslem2  33786  cyc3conja  33788  reofld  33974  rearchi  33977  nn0archi  33978  xrge0slmod  33979  dimval  34303  dimvalfi  34304  ply1degltdimlem  34324  algextdeglem8  34426  qtophaus  34538  iistmd  34604  xpinpreima  34608  xpinpreima2  34609  tpr2rico  34614  mndpluscn  34628  xrge0pluscn  34642  cnzh  34670  rezh  34671  qqhucn  34694  rrhcn  34699  cnrrext  34712  zrhre  34721  qqhre  34722  ismntop  34728  sigaex  34812  brsiga  34886  cntnevol  34931  voliune  34932  ddemeas  34939  1stmbfm  34962  2ndmbfm  34963  br2base  34971  dya2icoseg2  34980  dya2iocucvr  34986  carsgclctunlem2  35021  carsgclctunlem3  35022  sitgaddlemb  35050  eulerpartlemt  35073  eulerpartgbij  35074  eulerpartlemmf  35077  eulerpartlemgvv  35078  eulerpartlemgf  35081  eulerpart  35084  sseqmw  35093  sseqf  35094  sseqp1  35097  fiblem  35100  fibp1  35103  dstrvprob  35174  coinflipspace  35183  coinfliprv  35185  coinflippv  35186  ballotlem1  35189  ballotlem8  35239  circlemethhgt  35342  r11  35809  r12  35810  acwer1prc  35852  j0iso  36004  j00smo  36005  maxssj0  36006  j0ltalephlem  36007  j0ltaleph  36008  jf1o  36011  j0le  36019  k3n0j0lt  36020  jltalephlem  36025  jltaleph  36026  onvf1od  36035  usgrcyclgt2v  36067  iccllysconn  36182  rellysconn  36183  satf00  36306  fmla0  36314  msrid  36477  dfrdg2  36735  dfrdg4  36893  imagesset  36895  filnetlem3  37346  limsucncmpi  37411  ttciunun  37477  bj-babygodel  37651  bj-idres  38273  taupilem3  38432  icoreresf  38467  icoreelrnab  38469  relowlssretop  38478  poimirlem3  38733  poimirlem9  38739  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem27  38757  poimirlem28  38758  poimirlem31  38761  poimirlem32  38762  mblfinlem1  38767  ovoliunnfl  38772  voliunnfl  38774  mbfresfi  38776  dvtan  38780  itg2addnc  38784  ftc1anclem3  38805  areacirc  38823  fdc  38871  ismrer1  38964  reheibor  38965  rngomndo  39061  gidsn  39078  ac6s6f  39297  cnvref4  39474  dfcnvrefrels2  39732  dfcnvrefrels3  39733  dedths  40211  tendo0co2  42037  erng1r  42244  dvalveclem  42274  dva0g  42276  dvh0g  42360  sn-it0e0  43660  sn-0tie0  43708  2rexfrabdioph  43996  3rexfrabdioph  43997  4rexfrabdioph  43998  6rexfrabdioph  43999  7rexfrabdioph  44000  rencldnfi  44021  jm2.27dlem2  44210  wepwso  44243  dfac11  44257  pwssplit4  44284  frlmpwfi  44293  isnumbasgrplem3  44299  mpaaeu  44344  proot1mul  44388  proot1hash  44389  epirron  44448  oneptr  44449  ordeldif1o  44454  oaomoencom  44511  oenassex  44512  cnvcnvintabd  44792  cnvrcl0  44817  dfrtrcl5  44821  cotrcltrcl  44917  frege92  45147  seff  45485  prmunb2  45487  binomcxplemdvbinom  45529  binomcxplemcvg  45530  binomcxplemnotnn0  45532  permac8prim  46199  sumsnd  46248  islptre  46836  stoweidlem34  47249  stoweidlem37  47252  stirlinglem11  47299  stirlinglem12  47300  stirlinglem13  47301  fouriersw  47446  fundcmpsurbijinjpreimafv  48694  fundcmpsurinjimaid  48698  fmtnoinf  48826  gbowge7  49066  nnsum3primes4  49091  usgrexmpl12ngrlic  49342  gpgprismgr4cycllem2  49399  gpg5ngric  49431  2zrng0  49546  lmodn0  49812  zlmodzxzldeplem3  49819  lvecpsslmod  49824  0dig2pr01  49927  nelsubc3lem  50389  fuconuniqex2  50992  aacllem  51219  amgmwlem  51267