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 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  minimp-syllsimp  1622  ceqsexv2dOLD  3518  dtruALT2  5345  dtruOLD  5421  intasym  6109  relcoi2  6271  funres11  6618  cnvresid  6620  find  7896  fparlem1  8116  fparlem2  8117  dftpos4  8249  tposf12  8255  wfrlem14OLD  8341  tfr2b  8415  tz7.44lem1  8424  ord3  8502  xp01disjl  8509  on2recsfn  8684  on2recsov  8685  on2ind  8686  on3ind  8687  xpcomco  9081  sbthlem2  9103  fidomdm  9351  brwdom2  9592  epnsym  9628  inf3lem6  9652  cnfcom  9719  ttrclco  9737  ttrclselem2  9745  tz9.1c  9749  frr1  9778  r1tr  9795  r1ord3g  9798  rankwflemb  9812  r1elwf  9815  r1elss  9825  rankval3b  9845  onssr1  9850  inlresf  9933  inrresf  9935  djuin  9937  infxpenlem  10032  alephnbtwn  10090  alephordilem1  10092  alephfp  10127  dfac13  10162  pwsdompw  10222  infdjuabs  10224  ackbij1  10256  ackbij2  10261  r1om  10262  cflim2  10282  fin23lem27  10347  fin23lem29  10360  fin23lem30  10361  fin1a2lem6  10424  fin1a2lem7  10425  fin1a2lem13  10431  itunitc1  10439  itunitc  10440  ituniiun  10441  hsmexlem5  10449  axcc2lem  10455  axcc3  10457  zorn2lem6  10520  zorn2lem7  10521  ttukeylem6  10533  dmct  10543  iunfo  10558  cardval  10565  cardid  10566  alephom  10604  canthp1lem2  10672  gchaleph2  10691  r1limwun  10755  inaprc  10855  nqerf  10949  recmulnq  10983  dmrecnq  10987  halfnq  10995  genpdm  11021  reclem3pr  11068  axresscn  11167  axpre-sup  11188  1re  11240  0re  11242  00id  11415  addrid  11420  0cnALT  11475  renegcli  11549  zexALT  12613  uzn0  12874  xrinfmss  13331  axdc4uzlem  14006  facnn  14298  fac0  14299  hashgval  14356  hashinf  14358  hashresfn  14363  hashrabrsn  14395  hashrabsn01  14396  hashrabsn1  14397  hashp1i  14426  hash1snb  14442  hashxplem  14456  fi1uzind  14530  cshw1  14845  cats1fv  14883  s7f1o  14990  trclubgi  15021  cnrecnv  15189  rexanuz  15369  climdm  15575  lo1eq  15589  rlimeq  15590  sumsnf  15764  tanval  16151  rpnnen2lem11  16247  rpnnen  16250  sadadd2lem  16483  sadadd3  16485  sadaddlem  16490  sadasslem  16494  sadeq  16496  lcmgcdlem  16630  unbenlem  16933  prmreclem6  16946  vdwlem8  17013  vdwnnlem1  17020  0ram  17045  structcnvcnv  17177  prdsvallem  17473  prdsval  17474  prdsbas  17476  prdsplusg  17477  prdsmulr  17478  prdsvsca  17479  prdshom  17486  xpsfrn  17587  xpsff1o2  17588  catcoppccl  18135  catcfuccl  18136  catcxpccl  18224  tsrss  18604  gsumpropd2lem  18662  smndex2dnrinv  18898  mvdco  19431  efgmnvl  19700  efgval  19703  efgi0  19706  efgi1  19707  efgredeu  19738  0frgp  19765  abln0  19853  lt6abl  19881  gsumval3  19893  gsum2dlem2  19957  dprdres  20016  dmdprdsplit2lem  20033  ringn0  20276  isdrng2  20708  drngmclOLD  20716  drngid2  20717  cnfldplusf  21364  cnfldsub  21365  cnsubmlem  21387  cnsubglem  21388  cnmsubglem  21403  gzrngunitlem  21405  rge0srg  21411  zring0  21424  pzriprnglem10  21456  zzngim  21518  zrhpsgnmhm  21549  re0g  21577  pjfval  21671  pjpm  21673  psrplusg  21901  coe1sfi  22154  ply1plusgfvi  22182  marep01ma  22603  smadiadetlem1a  22606  smadiadetlem3lem2  22610  smadiadetlem3  22611  smadiadetlem4  22612  smadiadet  22613  indistpsALT  22956  tgrest  23102  leordtval2  23155  lmbr2  23202  cnprest  23232  lmff  23244  kgenidm  23490  tx1cn  23552  tx2cn  23553  ustbas  24171  psmetge0  24256  xmetge0  24288  qdensere  24713  cnblcld  24718  cnfldms  24719  cnfldtopn  24725  xrsdsre  24755  xrge0tsms  24779  iccpnfcnv  24898  xrhmeo  24900  cnheiborlem  24909  cnlmod  25096  recvs  25102  lmmbr2  25216  lmcau  25270  metsscmetcld  25272  cncms  25312  cnfldcusp  25314  ovolctb  25448  ovoliunnul  25465  ismbl  25484  volf  25487  voliunlem1  25508  ioorf  25531  ioorinv  25534  ioorcl  25535  dyaddisj  25554  dyadmax  25556  dyadmbl  25558  mbfid  25593  ismbfd  25597  mbfimaopnlem  25613  limcresi  25843  dvreslem  25867  dvres2lem  25868  dvcjbr  25910  dvferm1  25946  dvferm2  25948  dvlip2  25957  dv11cn  25963  deg1ldg  26054  deg1leb  26057  plycpn  26254  vieta1lem2  26276  elqaa  26287  aalioulem2  26298  aaliou3lem3  26309  aaliou3lem4  26311  pserulm  26388  psercnlem2  26391  psercnlem1  26392  psercn  26393  abelth  26408  reeff1o  26414  pilem1  26418  efhalfpi  26437  coseq0negpitopi  26469  pige3ALT  26486  tanregt0  26505  efif1olem3  26510  efif1olem4  26511  efifo  26513  eff1olem  26514  efsubm  26517  logrn  26524  ellogrn  26525  relogf1o  26532  argregt0  26576  argrege0  26577  dvrelog  26603  dvloglem  26614  logf1o2  26616  dvlog  26617  efopnlem1  26622  efopnlem2  26623  logtayl  26626  cxpcn3lem  26714  cxpcn3  26715  resqrtcn  26716  asinneg  26853  asinrebnd  26868  atan0  26875  atanbnd  26893  areambl  26925  sqrtlim  26940  amgmlem  26957  lgamucov  27005  basellem1  27048  basellem4  27051  sqff1o  27149  dchrplusg  27215  bposlem6  27257  bposlem8  27259  dchrvmasumlem2  27466  pntibndlem1  27557  pntlemo  27575  qrng0  27589  ostth  27607  noextendseq  27636  bday0s  27797  oldlim  27855  zsex  28325  lmif  28769  islmib  28771  structiedg0val  29006  snstriedgval  29022  umgredgnlp  29131  usgrexmplef  29243  usgrexmpledg  29246  vtxdlfgrval  29470  upgr2pthnlp  29719  konigsberglem5  30242  ex-mod  30435  pliguhgr  30472  grporn  30507  ip0i  30811  ubthlem1  30856  ubthlem2  30857  axhcompl-zf  30984  normlem7  31102  bcseqi  31106  bcsiALT  31165  hlimf  31223  hlimuni  31224  hhssabloilem  31247  hhshsslem1  31253  hhsssh  31255  hhsscms  31264  occllem  31289  occl  31290  h1deoi  31535  h1dei  31536  h1de2ctlem  31541  h1de2ci  31542  spansni  31543  spanunsni  31565  pjpythi  31708  nmfn0  31973  nmopadjlem  32075  adjcoi  32086  nmopcoadji  32087  pjoccoi  32164  shatomistici  32347  iuninc  32546  imadifxp  32587  xppreima  32628  1stpreima  32689  2ndpreima  32690  fsuppcurry1  32707  fsuppcurry2  32708  hashgt1  32792  s3clhash  32928  gsummpt2d  33048  xrge0tsmsd  33061  tocyc01  33134  cyc3evpm  33166  cycpmconjslem2  33171  cyc3conja  33173  reofld  33364  rearchi  33366  nn0archi  33367  xrge0slmod  33368  elrspunidl  33448  dimval  33645  dimvalfi  33646  ply1degltdimlem  33667  algextdeglem8  33763  qtophaus  33872  iistmd  33938  xpinpreima  33942  xpinpreima2  33943  tpr2rico  33948  mndpluscn  33962  xrge0pluscn  33976  cnzh  34004  rezh  34005  qqhucn  34028  rrhcn  34033  cnrrext  34046  zrhre  34055  qqhre  34056  ismntop  34062  sigaex  34146  brsiga  34219  cntnevol  34264  voliune  34265  ddemeas  34272  1stmbfm  34297  2ndmbfm  34298  br2base  34306  dya2icoseg2  34315  dya2iocucvr  34321  carsgclctunlem2  34356  carsgclctunlem3  34357  sitgaddlemb  34385  eulerpartlemt  34408  eulerpartgbij  34409  eulerpartlemmf  34412  eulerpartlemgvv  34413  eulerpartlemgf  34416  eulerpart  34419  sseqmw  34428  sseqf  34429  sseqp1  34432  fiblem  34435  fibp1  34438  dstrvprob  34509  coinflipspace  34518  coinfliprv  34520  coinflippv  34521  ballotlem1  34524  ballotlem8  34574  circlemethhgt  34680  usgrcyclgt2v  35158  iccllysconn  35277  rellysconn  35278  satf00  35401  fmla0  35409  msrid  35572  dfrdg2  35818  dfrdg4  35974  imagesset  35976  elhf  36197  filnetlem3  36403  limsucncmpi  36468  bj-babygodel  36626  bj-idres  37183  taupilem3  37342  icoreresf  37375  icoreelrnab  37377  relowlssretop  37386  poimirlem3  37652  poimirlem9  37658  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem27  37676  poimirlem28  37677  poimirlem31  37680  poimirlem32  37681  mblfinlem1  37686  ovoliunnfl  37691  voliunnfl  37693  mbfresfi  37695  dvtan  37699  itg2addnc  37703  ftc1anclem3  37724  areacirc  37742  fdc  37774  ismrer1  37867  reheibor  37868  rngomndo  37964  gidsn  37981  ac6s6f  38202  eccnvepex  38358  cnvref4  38373  dfcnvrefrels2  38551  dfcnvrefrels3  38552  dedths  38985  tendo0co2  40812  erng1r  41019  dvalveclem  41049  dva0g  41051  dvh0g  41135  sn-it0e0  42433  sn-0tie0  42457  2rexfrabdioph  42794  3rexfrabdioph  42795  4rexfrabdioph  42796  6rexfrabdioph  42797  7rexfrabdioph  42798  rencldnfi  42819  jm2.27dlem2  43009  wepwso  43042  dfac11  43061  pwssplit4  43088  frlmpwfi  43097  isnumbasgrplem3  43104  mpaaeu  43149  proot1mul  43193  proot1hash  43194  epirron  43253  oneptr  43254  ordeldif1o  43259  oaomoencom  43316  oenassex  43317  cnvcnvintabd  43599  cnvrcl0  43624  dfrtrcl5  43628  cotrcltrcl  43724  frege92  43954  seff  44308  prmunb2  44310  binomcxplemdvbinom  44352  binomcxplemcvg  44353  binomcxplemnotnn0  44355  permac8prim  45014  sumsnd  45030  islptre  45628  stoweidlem34  46043  stoweidlem37  46046  stirlinglem11  46093  stirlinglem12  46094  stirlinglem13  46095  fouriersw  46240  natlocalincr  46885  upwordsing  46893  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjimaid  47405  fmtnoinf  47530  gbowge7  47757  nnsum3primes4  47782  usgrexmpl12ngrlic  48023  gpgprismgr4cycllem2  48075  2zrng0  48199  lmodn0  48451  zlmodzxzldeplem3  48458  lvecpsslmod  48463  0dig2pr01  48570  nelsubc3lem  49017  aacllem  49645  amgmwlem  49646