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  1716  ceqsexv2d  3437  dtru  5040  intasym  5722  relcoi2  5877  funres11  6173  cnvresid  6175  idssxpOLD  6216  elnn  7301  omsinds  7310  fparlem1  7507  fparlem2  7508  dftpos4  7602  tposf12  7608  wfrlem14  7660  tfr2b  7724  tz7.44lem1  7733  xpcomco  8285  sbthlem2  8306  fidomdm  8478  hartogslem1  8682  brwdom2  8713  epnsym  8747  inf3lem6  8773  omex  8783  cnfcom  8840  tz9.1c  8849  r1tr  8882  r1ord3g  8885  rankwflemb  8899  r1elwf  8902  r1elss  8912  rankval3b  8932  onssr1  8937  inlresf  9019  inrresf  9021  djuin  9023  infxpenlem  9115  alephnbtwn  9173  alephordilem1  9175  alephfp  9210  dfac13  9245  pwsdompw  9307  infcdaabs  9309  ackbij1  9341  ackbij2  9346  r1om  9347  cflim2  9366  fin23lem27  9431  fin23lem29  9444  fin23lem30  9445  fin1a2lem6  9508  fin1a2lem7  9509  fin1a2lem13  9515  itunitc1  9523  itunitc  9524  ituniiun  9525  hsmexlem5  9533  axcc2lem  9539  axcc3  9541  zorn2lem6  9604  zorn2lem7  9605  ttukeylem6  9617  axdc  9624  fodom  9625  dmct  9627  iunfo  9642  cardval  9649  cardid  9650  pwcfsdom  9686  alephom  9688  canthp1lem2  9756  canthp1  9757  gchaleph2  9775  r1limwun  9839  inaprc  9939  nqerf  10033  recmulnq  10067  dmrecnq  10071  halfnq  10079  genpdm  10105  reclem3pr  10152  axresscn  10250  axpre-sup  10271  1re  10321  0re  10323  00id  10492  addid1  10497  renegcli  10623  zexALT  11658  uzn0  11916  dfle2  12192  xrinfmss  12354  xrge0neqmnfOLD  12492  axdc4uzlem  13002  facnn  13278  fac0  13279  hashgval  13336  hashinf  13338  hashresfn  13344  hashrabrsn  13375  hashrabsn01  13376  hashrabsn1  13377  hashp1i  13404  hashxplem  13433  fi1uzind  13492  cshw1  13788  cats1fv  13824  trclubgi  13957  cnrecnv  14124  rexanuz  14304  climdm  14504  lo1eq  14518  rlimeq  14519  sumsnf  14692  sumsn  14694  tanval  15074  rpnnen2lem11  15169  rpnnen  15172  sadadd2lem  15396  sadadd3  15398  sadaddlem  15403  sadasslem  15407  sadeq  15409  lcmgcdlem  15534  3prm  15620  unbenlem  15825  prmreclem6  15838  vdwlem8  15905  vdwnnlem1  15912  0ram  15937  structcnvcnv  16078  prdsval  16316  prdsbas  16318  prdsplusg  16319  prdsmulr  16320  prdsvsca  16321  prdshom  16328  xpsfrn  16430  xpsff1o2  16432  catcoppccl  16958  catcfuccl  16959  catcxpccl  17048  tsrss  17424  gsumpropd2lem  17474  symgid  18018  mvdco  18062  efgmnvl  18324  efgval  18327  efgi0  18330  efgi1  18331  efgredeu  18362  0frgp  18389  abln0  18467  lt6abl  18493  gsumval3  18505  gsum2dlem2  18567  dprdres  18625  dmdprdsplit2lem  18642  ringn0  18801  isdrng2  18957  drngmcl  18960  drngid2  18963  psrplusg  19586  coe1sfi  19787  ply1plusgfvi  19816  cnfldplusf  19977  cnfldsub  19978  cnsubmlem  19998  cnmsubglem  20013  gzrngunitlem  20015  rge0srg  20021  zring0  20032  zzngim  20104  zrhpsgnmhm  20133  re0g  20163  pjfval  20257  pjpm  20259  marep01ma  20675  smadiadetlem1a  20678  smadiadetlem3lem2  20682  smadiadetlem3  20683  smadiadetlem4  20684  smadiadet  20685  indistpsALT  21028  tgrest  21174  leordtval2  21227  lmbr2  21274  cnprest  21304  lmff  21316  kgenidm  21561  tx1cn  21623  tx2cn  21624  hausdiag  21659  elrnust  22238  ustbas  22241  psmetge0  22327  xmetge0  22359  qdensere  22783  cnblcld  22788  cnfldms  22789  cnfldtopn  22795  xrsdsre  22823  xrge0tsms  22847  iccpnfcnv  22953  xrhmeo  22955  cnheiborlem  22963  cnlmod  23149  lmmbr2  23267  lmcau  23321  cmetss  23323  cncms  23361  cnfldcusp  23363  ovolctb  23470  ovoliunnul  23487  ismbl  23506  volf  23509  voliunlem1  23530  ioorf  23553  ioorinv  23556  ioorcl  23557  dyaddisj  23576  dyadmax  23578  dyadmbl  23580  mbfid  23615  ismbfd  23619  mbfimaopnlem  23635  limcresi  23862  dvreslem  23886  dvres2lem  23887  dvcjbr  23925  dvferm1  23961  dvferm2  23963  dvlip2  23971  dv11cn  23977  deg1ldg  24065  deg1leb  24068  plycpn  24257  vieta1lem2  24279  elqaa  24290  aalioulem2  24301  aaliou3lem3  24312  aaliou3lem4  24314  pserulm  24389  psercnlem2  24391  psercnlem1  24392  psercn  24393  abelth  24408  reeff1o  24414  pilem1  24418  efhalfpi  24437  coseq0negpitopi  24469  pige3  24483  tanregt0  24499  efif1olem3  24504  efif1olem4  24505  efifo  24507  eff1olem  24508  efsubm  24511  logrn  24518  ellogrn  24519  relogf1o  24526  argregt0  24569  argrege0  24570  dvrelog  24596  dvloglem  24607  logf1o2  24609  dvlog  24610  efopnlem1  24615  efopnlem2  24616  logtayl  24619  cxpcn3lem  24701  cxpcn3  24702  resqrtcn  24703  asinneg  24826  asinrebnd  24841  atan0  24848  atanbnd  24866  areambl  24898  sqrtlim  24912  amgmlem  24929  lgamucov  24977  basellem1  25020  basellem4  25023  sqff1o  25121  dchrplusg  25185  bposlem6  25227  bposlem8  25229  dchrvmasumlem2  25400  mulog2sum  25439  pntibndlem1  25491  pntlemo  25509  qrng0  25523  ostth  25541  lmif  25890  islmib  25892  structiedg0val  26124  snstriedgval  26143  umgredgnlp  26256  usgrexmplef  26366  usgrexmpledg  26369  vtxdlfgrval  26608  upgr2pthnlp  26855  konigsberglem5  27428  ex-mod  27636  pliguhgr  27668  grporn  27703  ip0i  28007  ubthlem1  28053  ubthlem2  28054  axhcompl-zf  28182  normlem7  28300  bcseqi  28304  bcsiALT  28363  hlimf  28421  hlimuni  28422  hhssabloilem  28445  hhshsslem1  28451  hhsssh  28453  hhsscms  28463  occllem  28489  occl  28490  h1deoi  28735  h1dei  28736  h1de2ctlem  28741  h1de2ci  28742  spansni  28743  spanunsni  28765  pjpythi  28908  nmfn0  29173  nmopadjlem  29275  adjcoi  29286  nmopcoadji  29287  pjoccoi  29364  shatomistici  29547  imadifxp  29738  xppreima  29775  1stpreima  29810  2ndpreima  29811  gsummpt2d  30105  xrge0tsmsd  30109  reofld  30164  rearchi  30166  nn0archi  30167  xrge0slmod  30168  qtophaus  30227  iistmd  30272  xpinpreima  30276  xpinpreima2  30277  tpr2rico  30282  mndpluscn  30296  xrge0pluscn  30310  cnzh  30338  rezh  30339  qqhucn  30360  rrhcn  30365  cnrrext  30378  zrhre  30387  qqhre  30388  ismntop  30394  sigaex  30496  brsiga  30570  cntnevol  30615  voliune  30616  ddemeas  30623  1stmbfm  30646  2ndmbfm  30647  br2base  30655  dya2icoseg2  30664  dya2iocucvr  30670  carsgclctunlem2  30705  carsgclctunlem3  30706  sitgaddlemb  30734  eulerpartlemt  30757  eulerpartgbij  30758  eulerpartlemmf  30761  eulerpartlemgvv  30762  eulerpartlemgf  30765  eulerpart  30768  sseqmw  30777  sseqf  30778  sseqp1  30781  fiblem  30784  fibp1  30787  dstrvprob  30857  coinflipspace  30866  coinfliprv  30868  coinflippv  30869  ballotlem1  30872  ballotlem8  30922  circlemethhgt  31045  iccllysconn  31553  rellysconn  31554  msrid  31763  dfrdg2  32019  trpredlem1  32045  trpredtr  32048  trpredmintr  32049  noextendseq  32139  dfrdg4  32377  imagesset  32379  elhf  32600  filnetlem3  32694  limsucncmpi  32759  taupilem3  33480  icoreresf  33514  icoreelrnab  33516  relowlssretop  33525  poimirlem3  33723  poimirlem9  33729  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem27  33747  poimirlem28  33748  poimirlem31  33751  poimirlem32  33752  mblfinlem1  33757  ovoliunnfl  33762  voliunnfl  33764  mbfresfi  33766  dvtan  33770  itg2addnc  33774  ftc1anclem3  33797  areacirc  33815  fdc  33850  ismrer1  33946  reheibor  33947  rngomndo  34043  gidsn  34060  ac6s6f  34289  dfcnvrefrels2  34587  dfcnvrefrels3  34588  dedths  34739  tendo0co2  36566  erng1r  36773  dvalveclem  36803  dva0g  36805  dvh0g  36889  2rexfrabdioph  37859  3rexfrabdioph  37860  4rexfrabdioph  37861  6rexfrabdioph  37862  7rexfrabdioph  37863  rencldnfi  37884  jm2.27dlem2  38075  wepwso  38111  dfac11  38130  pwssplit4  38157  frlmpwfi  38166  isnumbasgrplem3  38173  mpaaeu  38218  proot1mul  38275  proot1hash  38276  cnvcnvintabd  38403  rtrclex  38421  cnvrcl0  38429  dfrtrcl5  38433  frege92  38746  seff  39005  prmunb2  39007  binomcxplemdvbinom  39049  binomcxplemcvg  39050  binomcxplemnotnn0  39052  sumsnd  39676  islptre  40328  stoweidlem34  40727  stoweidlem37  40730  stirlinglem11  40777  stirlinglem12  40778  stirlinglem13  40779  fouriersw  40924  fmtnoinf  42020  gbowge7  42223  nnsum3primes4  42248  2zrng0  42503  lmodn0  42849  zlmodzxzldeplem3  42856  lvecpsslmod  42861  0dig2pr01  42969  aacllem  43115  amgmwlem  43116