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  3491  dtruALT2  5312  dtruOLD  5388  intasym  6068  relcoi2  6229  funres11  6563  cnvresid  6565  find  7835  fparlem1  8052  fparlem2  8053  dftpos4  8185  tposf12  8191  tfr2b  8325  tz7.44lem1  8334  ord3  8410  xp01disjl  8417  on2recsfn  8592  on2recsov  8593  on2ind  8594  on3ind  8595  xpcomco  8991  sbthlem2  9012  fidomdm  9243  brwdom2  9484  epnsym  9524  inf3lem6  9548  cnfcom  9615  ttrclco  9633  ttrclselem2  9641  tz9.1c  9645  frr1  9674  r1tr  9691  r1ord3g  9694  rankwflemb  9708  r1elwf  9711  r1elss  9721  rankval3b  9741  onssr1  9746  inlresf  9829  inrresf  9831  djuin  9833  infxpenlem  9926  alephnbtwn  9984  alephordilem1  9986  alephfp  10021  dfac13  10056  pwsdompw  10116  infdjuabs  10118  ackbij1  10150  ackbij2  10155  r1om  10156  cflim2  10176  fin23lem27  10241  fin23lem29  10254  fin23lem30  10255  fin1a2lem6  10318  fin1a2lem7  10319  fin1a2lem13  10325  itunitc1  10333  itunitc  10334  ituniiun  10335  hsmexlem5  10343  axcc2lem  10349  axcc3  10351  zorn2lem6  10414  zorn2lem7  10415  ttukeylem6  10427  dmct  10437  iunfo  10452  cardval  10459  cardid  10460  alephom  10498  canthp1lem2  10566  gchaleph2  10585  r1limwun  10649  inaprc  10749  nqerf  10843  recmulnq  10877  dmrecnq  10881  halfnq  10889  genpdm  10915  reclem3pr  10962  axresscn  11061  axpre-sup  11082  1re  11134  0re  11136  00id  11309  addrid  11314  0cnALT  11369  renegcli  11443  zexALT  12509  uzn0  12770  xrinfmss  13230  axdc4uzlem  13908  facnn  14200  fac0  14201  hashgval  14258  hashinf  14260  hashresfn  14265  hashrabrsn  14297  hashrabsn01  14298  hashrabsn1  14299  hashp1i  14328  hash1snb  14344  hashxplem  14358  fi1uzind  14432  cshw1  14746  cats1fv  14784  s7f1o  14891  trclubgi  14922  cnrecnv  15090  rexanuz  15271  climdm  15479  lo1eq  15493  rlimeq  15494  sumsnf  15668  tanval  16055  rpnnen2lem11  16151  rpnnen  16154  sadadd2lem  16388  sadadd3  16390  sadaddlem  16395  sadasslem  16399  sadeq  16401  lcmgcdlem  16535  unbenlem  16838  prmreclem6  16851  vdwlem8  16918  vdwnnlem1  16925  0ram  16950  structcnvcnv  17082  prdsvallem  17376  prdsval  17377  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdshom  17389  xpsfrn  17490  xpsff1o2  17491  catcoppccl  18042  catcfuccl  18043  catcxpccl  18131  tsrss  18513  gsumpropd2lem  18571  smndex2dnrinv  18807  mvdco  19342  efgmnvl  19611  efgval  19614  efgi0  19617  efgi1  19618  efgredeu  19649  0frgp  19676  abln0  19764  lt6abl  19792  gsumval3  19804  gsum2dlem2  19868  dprdres  19927  dmdprdsplit2lem  19944  ringn0  20214  isdrng2  20646  drngmclOLD  20654  drngid2  20655  cnfldplusf  21321  cnfldsub  21322  cnsubmlem  21339  cnsubglem  21340  cnmsubglem  21355  gzrngunitlem  21357  rge0srg  21363  zring0  21383  pzriprnglem10  21415  zzngim  21477  zrhpsgnmhm  21509  re0g  21537  pjfval  21631  pjpm  21633  psrplusg  21861  coe1sfi  22114  ply1plusgfvi  22142  marep01ma  22563  smadiadetlem1a  22566  smadiadetlem3lem2  22570  smadiadetlem3  22571  smadiadetlem4  22572  smadiadet  22573  indistpsALT  22916  tgrest  23062  leordtval2  23115  lmbr2  23162  cnprest  23192  lmff  23204  kgenidm  23450  tx1cn  23512  tx2cn  23513  ustbas  24131  psmetge0  24216  xmetge0  24248  qdensere  24673  cnblcld  24678  cnfldms  24679  cnfldtopn  24685  xrsdsre  24715  xrge0tsms  24739  iccpnfcnv  24858  xrhmeo  24860  cnheiborlem  24869  cnlmod  25056  recvs  25062  lmmbr2  25175  lmcau  25229  metsscmetcld  25231  cncms  25271  cnfldcusp  25273  ovolctb  25407  ovoliunnul  25424  ismbl  25443  volf  25446  voliunlem1  25467  ioorf  25490  ioorinv  25493  ioorcl  25494  dyaddisj  25513  dyadmax  25515  dyadmbl  25517  mbfid  25552  ismbfd  25556  mbfimaopnlem  25572  limcresi  25802  dvreslem  25826  dvres2lem  25827  dvcjbr  25869  dvferm1  25905  dvferm2  25907  dvlip2  25916  dv11cn  25922  deg1ldg  26013  deg1leb  26016  plycpn  26213  vieta1lem2  26235  elqaa  26246  aalioulem2  26257  aaliou3lem3  26268  aaliou3lem4  26270  pserulm  26347  psercnlem2  26350  psercnlem1  26351  psercn  26352  abelth  26367  reeff1o  26373  pilem1  26377  efhalfpi  26396  coseq0negpitopi  26428  pige3ALT  26445  tanregt0  26464  efif1olem3  26469  efif1olem4  26470  efifo  26472  eff1olem  26473  efsubm  26476  logrn  26483  ellogrn  26484  relogf1o  26491  argregt0  26535  argrege0  26536  dvrelog  26562  dvloglem  26573  logf1o2  26575  dvlog  26576  efopnlem1  26581  efopnlem2  26582  logtayl  26585  cxpcn3lem  26673  cxpcn3  26674  resqrtcn  26675  asinneg  26812  asinrebnd  26827  atan0  26834  atanbnd  26852  areambl  26884  sqrtlim  26899  amgmlem  26916  lgamucov  26964  basellem1  27007  basellem4  27010  sqff1o  27108  dchrplusg  27174  bposlem6  27216  bposlem8  27218  dchrvmasumlem2  27425  pntibndlem1  27516  pntlemo  27534  qrng0  27548  ostth  27566  noextendseq  27595  bday0s  27760  oldlim  27819  zsex  28291  lmif  28748  islmib  28750  structiedg0val  28985  snstriedgval  29001  umgredgnlp  29110  usgrexmplef  29222  usgrexmpledg  29225  vtxdlfgrval  29449  upgr2pthnlp  29695  konigsberglem5  30218  ex-mod  30411  pliguhgr  30448  grporn  30483  ip0i  30787  ubthlem1  30832  ubthlem2  30833  axhcompl-zf  30960  normlem7  31078  bcseqi  31082  bcsiALT  31141  hlimf  31199  hlimuni  31200  hhssabloilem  31223  hhshsslem1  31229  hhsssh  31231  hhsscms  31240  occllem  31265  occl  31266  h1deoi  31511  h1dei  31512  h1de2ctlem  31517  h1de2ci  31518  spansni  31519  spanunsni  31541  pjpythi  31684  nmfn0  31949  nmopadjlem  32051  adjcoi  32062  nmopcoadji  32063  pjoccoi  32140  shatomistici  32323  iuninc  32522  imadifxp  32563  xppreima  32602  1stpreima  32663  2ndpreima  32664  fsuppcurry1  32681  fsuppcurry2  32682  hashgt1  32766  s3clhash  32902  gsummpt2d  33015  xrge0tsmsd  33028  tocyc01  33073  cyc3evpm  33105  cycpmconjslem2  33110  cyc3conja  33112  reofld  33291  rearchi  33293  nn0archi  33294  xrge0slmod  33295  elrspunidl  33375  dimval  33572  dimvalfi  33573  ply1degltdimlem  33594  algextdeglem8  33690  qtophaus  33802  iistmd  33868  xpinpreima  33872  xpinpreima2  33873  tpr2rico  33878  mndpluscn  33892  xrge0pluscn  33906  cnzh  33934  rezh  33935  qqhucn  33958  rrhcn  33963  cnrrext  33976  zrhre  33985  qqhre  33986  ismntop  33992  sigaex  34076  brsiga  34149  cntnevol  34194  voliune  34195  ddemeas  34202  1stmbfm  34227  2ndmbfm  34228  br2base  34236  dya2icoseg2  34245  dya2iocucvr  34251  carsgclctunlem2  34286  carsgclctunlem3  34287  sitgaddlemb  34315  eulerpartlemt  34338  eulerpartgbij  34339  eulerpartlemmf  34342  eulerpartlemgvv  34343  eulerpartlemgf  34346  eulerpart  34349  sseqmw  34358  sseqf  34359  sseqp1  34362  fiblem  34365  fibp1  34368  dstrvprob  34439  coinflipspace  34448  coinfliprv  34450  coinflippv  34451  ballotlem1  34454  ballotlem8  34504  circlemethhgt  34610  onvf1od  35079  usgrcyclgt2v  35103  iccllysconn  35222  rellysconn  35223  satf00  35346  fmla0  35354  msrid  35517  dfrdg2  35768  dfrdg4  35924  imagesset  35926  elhf  36147  filnetlem3  36353  limsucncmpi  36418  bj-babygodel  36576  bj-idres  37133  taupilem3  37292  icoreresf  37325  icoreelrnab  37327  relowlssretop  37336  poimirlem3  37602  poimirlem9  37608  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem27  37626  poimirlem28  37627  poimirlem31  37630  poimirlem32  37631  mblfinlem1  37636  ovoliunnfl  37641  voliunnfl  37643  mbfresfi  37645  dvtan  37649  itg2addnc  37653  ftc1anclem3  37674  areacirc  37692  fdc  37724  ismrer1  37817  reheibor  37818  rngomndo  37914  gidsn  37931  ac6s6f  38152  cnvref4  38317  dfcnvrefrels2  38504  dfcnvrefrels3  38505  dedths  38940  tendo0co2  40767  erng1r  40974  dvalveclem  41004  dva0g  41006  dvh0g  41090  sn-it0e0  42389  sn-0tie0  42424  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  rencldnfi  42794  jm2.27dlem2  42983  wepwso  43016  dfac11  43035  pwssplit4  43062  frlmpwfi  43071  isnumbasgrplem3  43078  mpaaeu  43123  proot1mul  43167  proot1hash  43168  epirron  43227  oneptr  43228  ordeldif1o  43233  oaomoencom  43290  oenassex  43291  cnvcnvintabd  43573  cnvrcl0  43598  dfrtrcl5  43602  cotrcltrcl  43698  frege92  43928  seff  44282  prmunb2  44284  binomcxplemdvbinom  44326  binomcxplemcvg  44327  binomcxplemnotnn0  44329  permac8prim  44988  sumsnd  45004  islptre  45601  stoweidlem34  46016  stoweidlem37  46019  stirlinglem11  46066  stirlinglem12  46067  stirlinglem13  46068  fouriersw  46213  natlocalincr  46858  upwordsing  46866  fundcmpsurbijinjpreimafv  47392  fundcmpsurinjimaid  47396  fmtnoinf  47521  gbowge7  47748  nnsum3primes4  47773  usgrexmpl12ngrlic  48024  gpgprismgr4cycllem2  48081  gpg5ngric  48113  2zrng0  48229  lmodn0  48481  zlmodzxzldeplem3  48488  lvecpsslmod  48493  0dig2pr01  48596  nelsubc3lem  49056  aacllem  49787  amgmwlem  49788