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  1654  dtruALT2  5331  intasym  6108  relcoi2  6280  funres11  6617  cnvresid  6619  find  7907  fparlem1  8125  fparlem2  8126  dftpos4  8265  tposf12  8271  tfr2b  8407  tz7.44lem1  8416  ord3  8495  xp01disjl  8503  on2recsfn  8679  on2recsov  8680  on2ind  8681  on3ind  8682  xpcomco  9089  sbthlem2  9110  fidomdm  9326  brwdom2  9570  epnsym  9613  inf3lem6  9637  cnfcom  9704  ttrclco  9722  ttrclselem2  9730  tz9.1c  9734  frr1  9766  r1tr  9786  r1ord3g  9789  rankwflembOLD  9804  r1elwf  9807  r1elss  9817  rankval3b  9839  onssr1  9846  elhfOLD  9911  inlresf  9998  inrresf  10000  djuin  10002  infxpenlem  10095  alephnbtwn  10153  alephordilem1  10155  alephfp  10190  dfac13  10224  pwsdompw  10284  infdjuabs  10286  ackbij1  10318  ackbij2  10323  cflim2  10344  fin23lem27  10409  fin23lem29  10422  fin23lem30  10423  fin1a2lem6  10486  fin1a2lem7  10487  fin1a2lem13  10493  itunitc1  10501  itunitc  10502  ituniiun  10503  hsmexlem5  10511  axcc2lem  10517  axcc3  10519  zorn2lem6  10582  zorn2lem7  10583  ttukeylem6  10595  dmct  10605  dmctOLD  10606  iunfo  10626  cardval  10633  cardid  10634  alephom  10673  canthp1lem2  10741  gchaleph2  10760  r1limwun  10824  inaprc  10924  nqerf  11018  recmulnq  11052  dmrecnq  11056  halfnq  11064  genpdm  11090  reclem3pr  11137  axresscn  11236  axpre-sup  11257  1re  11311  0re  11313  00id  11488  addrid  11493  0cnALT  11548  renegcli  11622  zexALT  12716  uzn0  12985  xrinfmss  13443  axdc4uzlem  14129  facnn  14422  fac0  14423  hashgval  14480  hashinf  14482  hashresfn  14487  hashrabrsn  14519  hashrabsn01  14520  hashrabsn1  14521  hashp1i  14550  hash1snb  14567  hashxplem  14581  fi1uzind  14655  cshw1  14977  cats1fv  15014  s7f1o  15124  trclubgi  15155  cnrecnv  15337  rexanuz  15518  climdm  15726  lo1eq  15740  rlimeq  15741  sumsnf  15914  tanval  16301  rpnnen2lem11  16397  rpnnen  16400  sadadd2lem  16634  sadadd3  16636  sadaddlem  16641  sadasslem  16645  sadeq  16647  lcmgcdlem  16786  unbenlem  17091  prmreclem6  17104  vdwlem8  17171  vdwnnlem1  17178  0ram  17203  structcnvcnv  17336  prdsvallem  17630  prdsval  17631  prdsbas  17633  prdsplusg  17634  prdsmulr  17635  prdsvsca  17636  prdshom  17643  xpsfrn  17745  xpsff1o2  17746  catcoppccl  18297  catcfuccl  18298  catcxpccl  18386  tsrss  18768  gsumpropd2lem  18873  smndex2dnrinv  19119  mvdco  19664  efgmnvl  19933  efgval  19936  efgi0  19939  efgi1  19940  efgredeu  19971  0frgp  19998  abln0  20086  lt6abl  20114  gsumval3  20126  gsum2dlem2  20190  dprdres  20249  dmdprdsplit2lem  20266  ringn0  20547  isdrng2  21002  drngid2  21015  cnfldplusf  21710  cnfldsub  21711  cnsubmlem  21726  cnsubglem  21727  cnmsubglem  21741  gzrngunitlem  21743  rge0srg  21749  zring0  21769  pzriprnglem10  21801  zzngim  21863  zrhpsgnmhm  21895  re0g  21923  pjfval  22017  pjpm  22019  psrplusg  22250  coe1sfi  22536  ply1plusgfvi  22564  marep01ma  22980  smadiadetlem1a  22983  smadiadetlem3lem2  22987  smadiadetlem3  22988  smadiadetlem4  22989  smadiadet  22990  indistpsALT  23336  tgrest  23482  leordtval2  23535  lmbr2  23582  cnprest  23612  lmff  23624  kgenidm  23871  tx1cn  23933  tx2cn  23934  ustbas  24551  psmetge0  24636  xmetge0  24668  qdensere  25093  cnblcld  25098  cnfldms  25099  cnfldtopn  25105  xrsdsre  25135  xrge0tsms  25159  iccpnfcnv  25270  xrhmeo  25272  cnheiborlem  25280  cnlmod  25466  recvs  25472  lmmbr2  25585  lmcau  25639  metsscmetcld  25641  cncms  25681  cnfldcusp  25683  ovolctb  25816  ovoliunnul  25833  ismbl  25852  volf  25855  voliunlem1  25876  ioorf  25899  ioorinv  25902  ioorcl  25903  dyaddisj  25922  dyadmax  25924  dyadmbl  25926  mbfid  25961  ismbfd  25965  mbfimaopnlem  25981  limcresi  26210  dvreslem  26234  dvres2lem  26235  dvcjbr  26274  dvferm1  26310  dvferm2  26312  dvlip2  26320  dv11cn  26326  deg1ldg  26415  deg1leb  26418  plycpn  26615  vieta1lem2  26639  elqaa  26650  aalioulem2  26665  aaliou3lem3  26676  aaliou3lem4  26678  pserulm  26754  psercnlem2  26756  psercnlem1  26757  psercn  26758  abelth  26773  reeff1o  26779  pilem1  26783  efhalfpi  26805  coseq0negpitopi  26837  pige3ALT  26853  tanregt0  26872  efif1olem3  26877  efif1olem4  26878  efifo  26880  eff1olem  26881  efsubm  26884  logrn  26891  ellogrn  26892  relogf1o  26899  argregt0  26943  argrege0  26944  dvrelog  26970  dvloglem  26981  logf1o2  26983  dvlog  26984  efopnlem1  26989  efopnlem2  26990  logtayl  26993  cxpcn3lem  27080  cxpcn3  27081  resqrtcn  27082  asinneg  27219  asinrebnd  27234  atan0  27241  atanbnd  27259  areambl  27291  sqrtlim  27305  amgmlem  27322  lgamucov  27370  basellem1  27413  basellem4  27416  sqff1o  27514  dchrplusg  27579  bposlem6  27621  bposlem8  27623  dchrvmasumlem2  27830  pntibndlem1  27921  pntlemo  27939  qrng0  27953  ostth  27971  noextendseq  28029  bday0  28202  oldlim  28278  ons2ind  28666  zsex  28771  lmif  29295  islmib  29297  structiedg0val  29605  snstriedgval  29621  umgredgnlp  29730  usgrexmplef  29845  usgrexmpledg  29848  vtxdlfgrval  30071  upgr2pthnlp  30323  konigsberglem5  30862  ex-mod  31055  nowisdomv  31080  pliguhgr  31093  grporn  31128  ip0i  31432  ubthlem1  31477  ubthlem2  31478  axhcompl-zf  31605  normlem7  31723  bcseqi  31727  bcsiALT  31786  hlimf  31844  hlimuni  31845  hhssabloilem  31868  hhshsslem1  31874  hhsssh  31876  hhsscms  31885  occllem  31910  occl  31911  h1deoi  32156  h1dei  32157  h1de2ctlem  32162  h1de2ci  32163  spansni  32164  spanunsni  32186  pjpythi  32329  nmfn0  32594  nmopadjlem  32696  adjcoi  32707  nmopcoadji  32708  pjoccoi  32785  shatomistici  32968  iuninc  33202  imadifxp  33242  xppreima  33286  1stpreima  33347  2ndpreima  33348  fsuppcurry1  33362  fsuppcurry2  33363  hashgt1  33446  s3clhash  33558  gsummpt2d  33656  xrge0tsmsd  33680  tocyc01  33725  cyc3evpm  33757  cycpmconjslem2  33762  cyc3conja  33764  reofld  33950  rearchi  33953  nn0archi  33954  xrge0slmod  33955  dimval  34279  dimvalfi  34280  ply1degltdimlem  34300  algextdeglem8  34402  qtophaus  34514  iistmd  34580  xpinpreima  34584  xpinpreima2  34585  tpr2rico  34590  mndpluscn  34604  xrge0pluscn  34618  cnzh  34646  rezh  34647  qqhucn  34670  rrhcn  34675  cnrrext  34688  zrhre  34697  qqhre  34698  ismntop  34704  sigaex  34788  brsiga  34862  cntnevol  34907  voliune  34908  ddemeas  34915  1stmbfm  34938  2ndmbfm  34939  br2base  34947  dya2icoseg2  34956  dya2iocucvr  34962  carsgclctunlem2  34997  carsgclctunlem3  34998  sitgaddlemb  35026  eulerpartlemt  35049  eulerpartgbij  35050  eulerpartlemmf  35053  eulerpartlemgvv  35054  eulerpartlemgf  35057  eulerpart  35060  sseqmw  35069  sseqf  35070  sseqp1  35073  fiblem  35076  fibp1  35079  dstrvprob  35150  coinflipspace  35159  coinfliprv  35161  coinflippv  35162  ballotlem1  35165  ballotlem8  35215  circlemethhgt  35318  r11  35777  r12  35778  acwer1prc  35816  j0iso  35943  j00smo  35944  maxssj0  35945  j0ltalephlem  35946  j0ltaleph  35947  onvf1od  35954  usgrcyclgt2v  35986  iccllysconn  36101  rellysconn  36102  satf00  36225  fmla0  36233  msrid  36396  dfrdg2  36649  dfrdg4  36807  imagesset  36809  filnetlem3  37260  limsucncmpi  37325  ttciunun  37391  bj-babygodel  37565  bj-idres  38174  taupilem3  38333  icoreresf  38368  icoreelrnab  38370  relowlssretop  38379  poimirlem3  38634  poimirlem9  38640  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem27  38658  poimirlem28  38659  poimirlem31  38662  poimirlem32  38663  mblfinlem1  38668  ovoliunnfl  38673  voliunnfl  38675  mbfresfi  38677  dvtan  38681  itg2addnc  38685  ftc1anclem3  38706  areacirc  38724  fdc  38772  ismrer1  38865  reheibor  38866  rngomndo  38962  gidsn  38979  ac6s6f  39198  cnvref4  39375  dfcnvrefrels2  39633  dfcnvrefrels3  39634  dedths  40112  tendo0co2  41938  erng1r  42145  dvalveclem  42175  dva0g  42177  dvh0g  42261  sn-it0e0  43560  sn-0tie0  43608  2rexfrabdioph  43896  3rexfrabdioph  43897  4rexfrabdioph  43898  6rexfrabdioph  43899  7rexfrabdioph  43900  rencldnfi  43921  jm2.27dlem2  44110  wepwso  44143  dfac11  44157  pwssplit4  44184  frlmpwfi  44193  isnumbasgrplem3  44200  mpaaeu  44245  proot1mul  44289  proot1hash  44290  epirron  44349  oneptr  44350  ordeldif1o  44355  oaomoencom  44412  oenassex  44413  cnvcnvintabd  44693  cnvrcl0  44718  dfrtrcl5  44722  cotrcltrcl  44818  frege92  45048  seff  45386  prmunb2  45388  binomcxplemdvbinom  45430  binomcxplemcvg  45431  binomcxplemnotnn0  45433  permac8prim  46097  sumsnd  46136  islptre  46724  stoweidlem34  47137  stoweidlem37  47140  stirlinglem11  47187  stirlinglem12  47188  stirlinglem13  47189  fouriersw  47334  fundcmpsurbijinjpreimafv  48582  fundcmpsurinjimaid  48586  fmtnoinf  48714  gbowge7  48954  nnsum3primes4  48979  usgrexmpl12ngrlic  49230  gpgprismgr4cycllem2  49287  gpg5ngric  49319  2zrng0  49434  lmodn0  49700  zlmodzxzldeplem3  49707  lvecpsslmod  49712  0dig2pr01  49815  nelsubc3lem  50277  fuconuniqex2  50880  aacllem  51107  amgmwlem  51155