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  5346  intasym  6120  relcoi2  6285  funres11  6620  cnvresid  6622  find  7901  fparlem1  8116  fparlem2  8117  dftpos4  8250  tposf12  8256  tfr2b  8392  tz7.44lem1  8401  ord3  8478  xp01disjl  8486  on2recsfn  8662  on2recsov  8663  on2ind  8664  on3ind  8665  xpcomco  9065  sbthlem2  9086  fidomdm  9301  brwdom2  9545  epnsym  9588  inf3lem6  9612  cnfcom  9679  ttrclco  9697  ttrclselem2  9705  tz9.1c  9709  frr1  9741  r1tr  9758  r1ord3g  9761  rankwflemb  9775  r1elwf  9778  r1elss  9788  rankval3b  9808  onssr1  9813  inlresf  9919  inrresf  9921  djuin  9923  infxpenlem  10016  alephnbtwn  10074  alephordilem1  10076  alephfp  10111  dfac13  10145  pwsdompw  10205  infdjuabs  10207  ackbij1  10239  ackbij2  10244  r1om  10245  cflim2  10265  fin23lem27  10330  fin23lem29  10343  fin23lem30  10344  fin1a2lem6  10407  fin1a2lem7  10408  fin1a2lem13  10414  itunitc1  10422  itunitc  10423  ituniiun  10424  hsmexlem5  10432  axcc2lem  10438  axcc3  10440  zorn2lem6  10503  zorn2lem7  10504  ttukeylem6  10516  dmct  10526  iunfo  10541  cardval  10548  cardid  10549  alephom  10588  canthp1lem2  10656  gchaleph2  10675  r1limwun  10739  inaprc  10839  nqerf  10933  recmulnq  10967  dmrecnq  10971  halfnq  10979  genpdm  11005  reclem3pr  11052  axresscn  11151  axpre-sup  11172  1re  11226  0re  11228  00id  11403  addrid  11408  0cnALT  11463  renegcli  11537  zexALT  12629  uzn0  12897  xrinfmss  13354  axdc4uzlem  14039  facnn  14331  fac0  14332  hashgval  14389  hashinf  14391  hashresfn  14396  hashrabrsn  14428  hashrabsn01  14429  hashrabsn1  14430  hashp1i  14459  hash1snb  14476  hashxplem  14490  fi1uzind  14564  cshw1  14885  cats1fv  14922  s7f1o  15029  trclubgi  15060  cnrecnv  15242  rexanuz  15423  climdm  15631  lo1eq  15645  rlimeq  15646  sumsnf  15820  tanval  16209  rpnnen2lem11  16305  rpnnen  16308  sadadd2lem  16542  sadadd3  16544  sadaddlem  16549  sadasslem  16553  sadeq  16555  lcmgcdlem  16689  unbenlem  16993  prmreclem6  17006  vdwlem8  17073  vdwnnlem1  17080  0ram  17105  structcnvcnv  17238  prdsvallem  17532  prdsval  17533  prdsbas  17535  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  prdshom  17545  xpsfrn  17647  xpsff1o2  17648  catcoppccl  18199  catcfuccl  18200  catcxpccl  18288  tsrss  18670  gsumpropd2lem  18766  smndex2dnrinv  19008  mvdco  19546  efgmnvl  19815  efgval  19818  efgi0  19821  efgi1  19822  efgredeu  19853  0frgp  19880  abln0  19968  lt6abl  19996  gsumval3  20008  gsum2dlem2  20072  dprdres  20131  dmdprdsplit2lem  20148  ringn0  20427  isdrng2  20880  drngid2  20893  cnfldplusf  21586  cnfldsub  21587  cnsubmlem  21602  cnsubglem  21603  cnmsubglem  21617  gzrngunitlem  21619  rge0srg  21625  zring0  21645  pzriprnglem10  21677  zzngim  21739  zrhpsgnmhm  21771  re0g  21799  pjfval  21893  pjpm  21895  psrplusg  22124  coe1sfi  22410  ply1plusgfvi  22438  marep01ma  22854  smadiadetlem1a  22857  smadiadetlem3lem2  22861  smadiadetlem3  22862  smadiadetlem4  22863  smadiadet  22864  indistpsALT  23207  tgrest  23353  leordtval2  23406  lmbr2  23453  cnprest  23483  lmff  23495  kgenidm  23741  tx1cn  23803  tx2cn  23804  ustbas  24421  psmetge0  24506  xmetge0  24538  qdensere  24963  cnblcld  24968  cnfldms  24969  cnfldtopn  24975  xrsdsre  25005  xrge0tsms  25029  iccpnfcnv  25140  xrhmeo  25142  cnheiborlem  25150  cnlmod  25336  recvs  25342  lmmbr2  25455  lmcau  25509  metsscmetcld  25511  cncms  25551  cnfldcusp  25553  ovolctb  25686  ovoliunnul  25703  ismbl  25722  volf  25725  voliunlem1  25746  ioorf  25769  ioorinv  25772  ioorcl  25773  dyaddisj  25792  dyadmax  25794  dyadmbl  25796  mbfid  25831  ismbfd  25835  mbfimaopnlem  25851  limcresi  26081  dvreslem  26105  dvres2lem  26106  dvcjbr  26145  dvferm1  26181  dvferm2  26183  dvlip2  26191  dv11cn  26197  deg1ldg  26286  deg1leb  26289  plycpn  26487  vieta1lem2  26509  elqaa  26520  aalioulem2  26533  aaliou3lem3  26544  aaliou3lem4  26546  pserulm  26622  psercnlem2  26624  psercnlem1  26625  psercn  26626  abelth  26641  reeff1o  26647  pilem1  26651  efhalfpi  26673  coseq0negpitopi  26705  pige3ALT  26722  tanregt0  26741  efif1olem3  26746  efif1olem4  26747  efifo  26749  eff1olem  26750  efsubm  26753  logrn  26760  ellogrn  26761  relogf1o  26768  argregt0  26812  argrege0  26813  dvrelog  26839  dvloglem  26850  logf1o2  26852  dvlog  26853  efopnlem1  26858  efopnlem2  26859  logtayl  26862  cxpcn3lem  26949  cxpcn3  26950  resqrtcn  26951  asinneg  27088  asinrebnd  27103  atan0  27110  atanbnd  27128  areambl  27160  sqrtlim  27174  amgmlem  27191  lgamucov  27239  basellem1  27282  basellem4  27285  sqff1o  27383  dchrplusg  27448  bposlem6  27490  bposlem8  27492  dchrvmasumlem2  27699  pntibndlem1  27790  pntlemo  27808  qrng0  27822  ostth  27840  noextendseq  27868  bday0  28041  oldlim  28117  ons2ind  28505  zsex  28610  lmif  29131  islmib  29133  structiedg0val  29409  snstriedgval  29425  umgredgnlp  29534  usgrexmplef  29646  usgrexmpledg  29649  vtxdlfgrval  29872  upgr2pthnlp  30118  konigsberglem5  30644  ex-mod  30837  nowisdomv  30862  pliguhgr  30875  grporn  30910  ip0i  31214  ubthlem1  31259  ubthlem2  31260  axhcompl-zf  31387  normlem7  31505  bcseqi  31509  bcsiALT  31568  hlimf  31626  hlimuni  31627  hhssabloilem  31650  hhshsslem1  31656  hhsssh  31658  hhsscms  31667  occllem  31692  occl  31693  h1deoi  31938  h1dei  31939  h1de2ctlem  31944  h1de2ci  31945  spansni  31946  spanunsni  31968  pjpythi  32111  nmfn0  32376  nmopadjlem  32478  adjcoi  32489  nmopcoadji  32490  pjoccoi  32567  shatomistici  32750  iuninc  32942  imadifxp  32983  xppreima  33027  1stpreima  33089  2ndpreima  33090  fsuppcurry1  33106  fsuppcurry2  33107  hashgt1  33190  s3clhash  33302  gsummpt2d  33400  xrge0tsmsd  33424  tocyc01  33469  cyc3evpm  33501  cycpmconjslem2  33506  cyc3conja  33508  reofld  33694  rearchi  33697  nn0archi  33698  xrge0slmod  33699  elrspunidl  33767  dimval  34022  dimvalfi  34023  ply1degltdimlem  34043  algextdeglem8  34145  qtophaus  34257  iistmd  34323  xpinpreima  34327  xpinpreima2  34328  tpr2rico  34333  mndpluscn  34347  xrge0pluscn  34361  cnzh  34389  rezh  34390  qqhucn  34413  rrhcn  34418  cnrrext  34431  zrhre  34440  qqhre  34441  ismntop  34447  sigaex  34531  brsiga  34604  cntnevol  34649  voliune  34650  ddemeas  34657  1stmbfm  34681  2ndmbfm  34682  br2base  34690  dya2icoseg2  34699  dya2iocucvr  34705  carsgclctunlem2  34740  carsgclctunlem3  34741  sitgaddlemb  34769  eulerpartlemt  34792  eulerpartgbij  34793  eulerpartlemmf  34796  eulerpartlemgvv  34797  eulerpartlemgf  34800  eulerpart  34803  sseqmw  34812  sseqf  34813  sseqp1  34816  fiblem  34819  fibp1  34822  dstrvprob  34893  coinflipspace  34902  coinfliprv  34904  coinflippv  34905  ballotlem1  34908  ballotlem8  34958  circlemethhgt  35061  r11  35511  r12  35512  onvf1od  35614  usgrcyclgt2v  35643  iccllysconn  35762  rellysconn  35763  satf00  35886  fmla0  35894  msrid  36057  dfrdg2  36305  dfrdg4  36463  imagesset  36465  elhf  36686  filnetlem3  36931  limsucncmpi  36996  ttciunun  37062  bj-babygodel  37236  bj-idres  37844  taupilem3  38003  icoreresf  38038  icoreelrnab  38040  relowlssretop  38049  poimirlem3  38314  poimirlem9  38320  poimirlem15  38326  poimirlem16  38327  poimirlem17  38328  poimirlem19  38330  poimirlem27  38338  poimirlem28  38339  poimirlem31  38342  poimirlem32  38343  mblfinlem1  38348  ovoliunnfl  38353  voliunnfl  38355  mbfresfi  38357  dvtan  38361  itg2addnc  38365  ftc1anclem3  38386  areacirc  38404  fdc  38436  ismrer1  38529  reheibor  38530  rngomndo  38626  gidsn  38643  ac6s6f  38862  cnvref4  39039  dfcnvrefrels2  39297  dfcnvrefrels3  39298  dedths  39776  tendo0co2  41602  erng1r  41809  dvalveclem  41839  dva0g  41841  dvh0g  41925  sn-it0e0  43217  sn-0tie0  43265  2rexfrabdioph  43563  3rexfrabdioph  43564  4rexfrabdioph  43565  6rexfrabdioph  43566  7rexfrabdioph  43567  rencldnfi  43588  jm2.27dlem2  43777  wepwso  43810  dfac11  43829  pwssplit4  43856  frlmpwfi  43865  isnumbasgrplem3  43872  mpaaeu  43917  proot1mul  43961  proot1hash  43962  epirron  44021  oneptr  44022  ordeldif1o  44027  oaomoencom  44084  oenassex  44085  cnvcnvintabd  44366  cnvrcl0  44391  dfrtrcl5  44395  cotrcltrcl  44491  frege92  44721  seff  45059  prmunb2  45061  binomcxplemdvbinom  45103  binomcxplemcvg  45104  binomcxplemnotnn0  45106  permac8prim  45763  sumsnd  45786  islptre  46375  stoweidlem34  46788  stoweidlem37  46791  stirlinglem11  46838  stirlinglem12  46839  stirlinglem13  46840  fouriersw  46985  natlocalincr  47632  fundcmpsurbijinjpreimafv  48196  fundcmpsurinjimaid  48200  fmtnoinf  48328  gbowge7  48568  nnsum3primes4  48593  usgrexmpl12ngrlic  48844  gpgprismgr4cycllem2  48901  gpg5ngric  48933  2zrng0  49049  lmodn0  49315  zlmodzxzldeplem3  49322  lvecpsslmod  49327  0dig2pr01  49430  nelsubc3lem  49888  aacllem  50661  amgmwlem  50690