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  1586  ceqsexv2d  3458  dtru  5121  intasym  5813  relcoi2  5964  funres11  6262  cnvresid  6264  elnn  7405  omsinds  7414  fparlem1  7614  fparlem2  7615  dftpos4  7713  tposf12  7719  wfrlem14  7771  tfr2b  7835  tz7.44lem1  7844  xp01disjl  7922  xpcomco  8402  sbthlem2  8423  fidomdm  8595  brwdom2  8831  epnsym  8865  inf3lem6  8889  omex  8899  cnfcom  8956  tz9.1c  8965  r1tr  8998  r1ord3g  9001  rankwflemb  9015  r1elwf  9018  r1elss  9028  rankval3b  9048  onssr1  9053  inlresf  9136  inrresf  9138  djuin  9140  infxpenlem  9232  alephnbtwn  9290  alephordilem1  9292  alephfp  9327  dfac13  9361  pwsdompw  9423  infdjuabs  9425  ackbij1  9457  ackbij2  9462  r1om  9463  cflim2  9482  fin23lem27  9547  fin23lem29  9560  fin23lem30  9561  fin1a2lem6  9624  fin1a2lem7  9625  fin1a2lem13  9631  itunitc1  9639  itunitc  9640  ituniiun  9641  hsmexlem5  9649  axcc2lem  9655  axcc3  9657  zorn2lem6  9720  zorn2lem7  9721  ttukeylem6  9733  axdc  9740  fodom  9741  dmct  9743  iunfo  9758  cardval  9765  cardid  9766  pwcfsdom  9802  alephom  9804  canthp1lem2  9872  gchaleph2  9891  r1limwun  9955  inaprc  10055  nqerf  10149  recmulnq  10183  dmrecnq  10187  halfnq  10195  genpdm  10221  reclem3pr  10268  axresscn  10367  axpre-sup  10388  1re  10438  0re  10440  0reOLD  10441  00id  10614  addid1  10619  0cnALT  10673  renegcli  10747  zexALT  11812  uzn0  12073  xrinfmss  12518  axdc4uzlem  13165  facnn  13449  fac0  13450  hashgval  13507  hashinf  13509  hashresfn  13514  hashrabrsn  13545  hashrabsn01  13546  hashrabsn1  13547  hashp1i  13576  hash1snb  13592  hashxplem  13606  fi1uzind  13665  cshw1  14045  cats1fv  14082  trclubgi  14217  cnrecnv  14384  rexanuz  14565  climdm  14771  lo1eq  14785  rlimeq  14786  sumsnf  14958  tanval  15340  rpnnen2lem11  15436  rpnnen  15439  sadadd2lem  15667  sadadd3  15669  sadaddlem  15674  sadasslem  15678  sadeq  15680  lcmgcdlem  15805  unbenlem  16099  prmreclem6  16112  vdwlem8  16179  vdwnnlem1  16186  0ram  16211  structcnvcnv  16352  prdsval  16583  prdsbas  16585  prdsplusg  16586  prdsmulr  16587  prdsvsca  16588  prdshom  16595  xpsfrncda  16706  xpsff1o2cda  16707  xpsfrn  16710  xpsff1o2  16711  catcoppccl  17239  catcfuccl  17240  catcxpccl  17328  tsrss  17704  gsumpropd2lem  17754  symgid  18303  mvdco  18347  efgmnvl  18611  efgval  18614  efgi0  18617  efgi1  18618  efgredeu  18651  0frgp  18678  abln0  18756  lt6abl  18782  gsumval3  18794  gsum2dlem2  18857  dprdres  18913  dmdprdsplit2lem  18930  ringn0  19089  isdrng2  19248  drngmcl  19251  drngid2  19254  psrplusg  19888  coe1sfi  20100  ply1plusgfvi  20129  cnfldplusf  20290  cnfldsub  20291  cnsubmlem  20311  cnsubglem  20312  cnmsubglem  20326  gzrngunitlem  20328  rge0srg  20334  zring0  20345  zzngim  20417  zrhpsgnmhm  20446  re0g  20474  pjfval  20568  pjpm  20570  marep01ma  20989  smadiadetlem1a  20992  smadiadetlem3lem2  20996  smadiadetlem3  20997  smadiadetlem4  20998  smadiadet  20999  indistpsALT  21341  tgrest  21487  leordtval2  21540  lmbr2  21587  cnprest  21617  lmff  21629  kgenidm  21875  tx1cn  21937  tx2cn  21938  elrnust  22552  ustbas  22555  psmetge0  22641  xmetge0  22673  qdensere  23097  cnblcld  23102  cnfldms  23103  cnfldtopn  23109  xrsdsre  23137  xrge0tsms  23161  iccpnfcnv  23267  xrhmeo  23269  cnheiborlem  23277  cnlmod  23463  lmmbr2  23581  lmcau  23635  metsscmetcld  23637  cncms  23677  cnfldcusp  23679  ovolctb  23810  ovoliunnul  23827  ismbl  23846  volf  23849  voliunlem1  23870  ioorf  23893  ioorinv  23896  ioorcl  23897  dyaddisj  23916  dyadmax  23918  dyadmbl  23920  mbfid  23955  ismbfd  23959  mbfimaopnlem  23975  limcresi  24202  dvreslem  24226  dvres2lem  24227  dvcjbr  24265  dvferm1  24301  dvferm2  24303  dvlip2  24311  dv11cn  24317  deg1ldg  24405  deg1leb  24408  plycpn  24597  vieta1lem2  24619  elqaa  24630  aalioulem2  24641  aaliou3lem3  24652  aaliou3lem4  24654  pserulm  24729  psercnlem2  24731  psercnlem1  24732  psercn  24733  abelth  24748  reeff1o  24754  pilem1  24758  efhalfpi  24776  coseq0negpitopi  24808  pige3ALT  24824  tanregt0  24840  efif1olem3  24845  efif1olem4  24846  efifo  24848  eff1olem  24849  efsubm  24852  logrn  24859  ellogrn  24860  relogf1o  24867  argregt0  24910  argrege0  24911  dvrelog  24937  dvloglem  24948  logf1o2  24950  dvlog  24951  efopnlem1  24956  efopnlem2  24957  logtayl  24960  cxpcn3lem  25045  cxpcn3  25046  resqrtcn  25047  asinneg  25181  asinrebnd  25196  atan0  25203  atanbnd  25221  areambl  25254  sqrtlim  25268  amgmlem  25285  lgamucov  25333  basellem1  25376  basellem4  25379  sqff1o  25477  dchrplusg  25541  bposlem6  25583  bposlem8  25585  dchrvmasumlem2  25792  mulog2sum  25831  pntibndlem1  25883  pntlemo  25901  qrng0  25915  ostth  25933  lmif  26289  islmib  26291  structiedg0val  26526  snstriedgval  26542  umgredgnlp  26651  usgrexmplef  26760  usgrexmpledg  26763  vtxdlfgrval  26986  upgr2pthnlp  27237  konigsberglem5  27804  ex-mod  28022  pliguhgr  28056  grporn  28091  ip0i  28395  ubthlem1  28441  ubthlem2  28442  axhcompl-zf  28570  normlem7  28688  bcseqi  28692  bcsiALT  28751  hlimf  28809  hlimuni  28810  hhssabloilem  28833  hhshsslem1  28839  hhsssh  28841  hhsscms  28851  occllem  28877  occl  28878  h1deoi  29123  h1dei  29124  h1de2ctlem  29129  h1de2ci  29130  spansni  29131  spanunsni  29153  pjpythi  29296  nmfn0  29561  nmopadjlem  29663  adjcoi  29674  nmopcoadji  29675  pjoccoi  29752  shatomistici  29935  iuninc  30099  imadifxp  30135  xppreima  30174  1stpreima  30219  2ndpreima  30220  fsuppcurry1  30238  fsuppcurry2  30239  s3clhash  30391  cyc3evpm  30496  gsummpt2d  30557  xrge0tsmsd  30563  reofld  30625  rearchi  30627  nn0archi  30628  xrge0slmod  30629  dimval  30663  dimvalfi  30664  qtophaus  30777  iistmd  30822  xpinpreima  30826  xpinpreima2  30827  tpr2rico  30832  mndpluscn  30846  xrge0pluscn  30860  cnzh  30888  rezh  30889  qqhucn  30910  rrhcn  30915  cnrrext  30928  zrhre  30937  qqhre  30938  ismntop  30944  sigaex  31046  brsiga  31120  cntnevol  31165  voliune  31166  ddemeas  31173  1stmbfm  31196  2ndmbfm  31197  br2base  31205  dya2icoseg2  31214  dya2iocucvr  31220  carsgclctunlem2  31255  carsgclctunlem3  31256  sitgaddlemb  31284  eulerpartlemt  31307  eulerpartgbij  31308  eulerpartlemmf  31311  eulerpartlemgvv  31312  eulerpartlemgf  31315  eulerpart  31318  sseqmw  31328  sseqf  31329  sseqp1  31332  fiblem  31335  fibp1  31338  dstrvprob  31408  coinflipspace  31417  coinfliprv  31419  coinflippv  31420  ballotlem1  31423  ballotlem8  31473  circlemethhgt  31595  iccllysconn  32115  rellysconn  32116  satf00  32217  fmla0  32225  msrid  32345  dfrdg2  32594  trpredlem1  32620  trpredtr  32623  trpredmintr  32624  noextendseq  32728  dfrdg4  32966  imagesset  32968  elhf  33189  filnetlem3  33282  limsucncmpi  33346  bj-babygodel  33487  taupilem3  34075  icoreresf  34108  icoreelrnab  34110  relowlssretop  34119  poimirlem3  34369  poimirlem9  34375  poimirlem15  34381  poimirlem16  34382  poimirlem17  34383  poimirlem19  34385  poimirlem27  34393  poimirlem28  34394  poimirlem31  34397  poimirlem32  34398  mblfinlem1  34403  ovoliunnfl  34408  voliunnfl  34410  mbfresfi  34412  dvtan  34416  itg2addnc  34420  ftc1anclem3  34443  areacirc  34461  fdc  34495  ismrer1  34591  reheibor  34592  rngomndo  34688  gidsn  34705  ac6s6f  34928  eccnvepex  35070  dfcnvrefrels2  35244  dfcnvrefrels3  35245  dedths  35576  tendo0co2  37402  erng1r  37609  dvalveclem  37639  dva0g  37641  dvh0g  37725  sn-dtru  38590  2rexfrabdioph  38823  3rexfrabdioph  38824  4rexfrabdioph  38825  6rexfrabdioph  38826  7rexfrabdioph  38827  rencldnfi  38848  jm2.27dlem2  39037  wepwso  39073  dfac11  39092  pwssplit4  39119  frlmpwfi  39128  isnumbasgrplem3  39135  mpaaeu  39180  proot1mul  39229  proot1hash  39230  cnvcnvintabd  39356  rtrclex  39374  cnvrcl0  39382  dfrtrcl5  39386  frege92  39698  seff  40091  prmunb2  40093  binomcxplemdvbinom  40135  binomcxplemcvg  40136  binomcxplemnotnn0  40138  sumsnd  40736  islptre  41361  stoweidlem34  41780  stoweidlem37  41783  stirlinglem11  41830  stirlinglem12  41831  stirlinglem13  41832  fouriersw  41977  fmtnoinf  43096  gbowge7  43326  nnsum3primes4  43351  2zrng0  43603  lmodn0  43947  zlmodzxzldeplem3  43954  lvecpsslmod  43959  0dig2pr01  44068  aacllem  44299  amgmwlem  44300