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  1629  ceqsexv2dOLD  3483  dtruALT2  5306  intasym  6072  relcoi2  6235  funres11  6569  cnvresid  6571  find  7842  fparlem1  8058  fparlem2  8059  dftpos4  8192  tposf12  8198  tfr2b  8332  tz7.44lem1  8341  ord3  8417  xp01disjl  8424  on2recsfn  8600  on2recsov  8601  on2ind  8602  on3ind  8603  xpcomco  9002  sbthlem2  9023  fidomdm  9241  brwdom2  9485  epnsym  9528  inf3lem6  9552  cnfcom  9619  ttrclco  9637  ttrclselem2  9645  tz9.1c  9649  frr1  9681  r1tr  9698  r1ord3g  9701  rankwflemb  9715  r1elwf  9718  r1elss  9728  rankval3b  9748  onssr1  9753  inlresf  9836  inrresf  9838  djuin  9840  infxpenlem  9933  alephnbtwn  9991  alephordilem1  9993  alephfp  10028  dfac13  10063  pwsdompw  10123  infdjuabs  10125  ackbij1  10157  ackbij2  10162  r1om  10163  cflim2  10183  fin23lem27  10248  fin23lem29  10261  fin23lem30  10262  fin1a2lem6  10325  fin1a2lem7  10326  fin1a2lem13  10332  itunitc1  10340  itunitc  10341  ituniiun  10342  hsmexlem5  10350  axcc2lem  10356  axcc3  10358  zorn2lem6  10421  zorn2lem7  10422  ttukeylem6  10434  dmct  10444  iunfo  10459  cardval  10466  cardid  10467  alephom  10506  canthp1lem2  10574  gchaleph2  10593  r1limwun  10657  inaprc  10757  nqerf  10851  recmulnq  10885  dmrecnq  10889  halfnq  10897  genpdm  10923  reclem3pr  10970  axresscn  11069  axpre-sup  11090  1re  11142  0re  11144  00id  11319  addrid  11324  0cnALT  11379  renegcli  11453  zexALT  12542  uzn0  12803  xrinfmss  13260  axdc4uzlem  13943  facnn  14235  fac0  14236  hashgval  14293  hashinf  14295  hashresfn  14300  hashrabrsn  14332  hashrabsn01  14333  hashrabsn1  14334  hashp1i  14363  hash1snb  14379  hashxplem  14393  fi1uzind  14467  cshw1  14782  cats1fv  14819  s7f1o  14926  trclubgi  14957  cnrecnv  15125  rexanuz  15306  climdm  15514  lo1eq  15528  rlimeq  15529  sumsnf  15703  tanval  16093  rpnnen2lem11  16189  rpnnen  16192  sadadd2lem  16426  sadadd3  16428  sadaddlem  16433  sadasslem  16437  sadeq  16439  lcmgcdlem  16573  unbenlem  16877  prmreclem6  16890  vdwlem8  16957  vdwnnlem1  16964  0ram  16989  structcnvcnv  17121  prdsvallem  17415  prdsval  17416  prdsbas  17418  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  prdshom  17428  xpsfrn  17530  xpsff1o2  17531  catcoppccl  18082  catcfuccl  18083  catcxpccl  18171  tsrss  18553  gsumpropd2lem  18645  smndex2dnrinv  18884  mvdco  19418  efgmnvl  19687  efgval  19690  efgi0  19693  efgi1  19694  efgredeu  19725  0frgp  19752  abln0  19840  lt6abl  19868  gsumval3  19880  gsum2dlem2  19944  dprdres  20003  dmdprdsplit2lem  20020  ringn0  20290  isdrng2  20722  drngmclOLD  20730  drngid2  20731  cnfldplusf  21381  cnfldsub  21382  cnsubmlem  21397  cnsubglem  21398  cnmsubglem  21412  gzrngunitlem  21414  rge0srg  21420  zring0  21440  pzriprnglem10  21472  zzngim  21534  zrhpsgnmhm  21566  re0g  21594  pjfval  21688  pjpm  21690  psrplusg  21919  coe1sfi  22205  ply1plusgfvi  22233  marep01ma  22650  smadiadetlem1a  22653  smadiadetlem3lem2  22657  smadiadetlem3  22658  smadiadetlem4  22659  smadiadet  22660  indistpsALT  23003  tgrest  23149  leordtval2  23202  lmbr2  23249  cnprest  23279  lmff  23291  kgenidm  23537  tx1cn  23599  tx2cn  23600  ustbas  24217  psmetge0  24302  xmetge0  24334  qdensere  24759  cnblcld  24764  cnfldms  24765  cnfldtopn  24771  xrsdsre  24801  xrge0tsms  24825  iccpnfcnv  24936  xrhmeo  24938  cnheiborlem  24946  cnlmod  25132  recvs  25138  lmmbr2  25251  lmcau  25305  metsscmetcld  25307  cncms  25347  cnfldcusp  25349  ovolctb  25482  ovoliunnul  25499  ismbl  25518  volf  25521  voliunlem1  25542  ioorf  25565  ioorinv  25568  ioorcl  25569  dyaddisj  25588  dyadmax  25590  dyadmbl  25592  mbfid  25627  ismbfd  25631  mbfimaopnlem  25647  limcresi  25877  dvreslem  25901  dvres2lem  25902  dvcjbr  25941  dvferm1  25977  dvferm2  25979  dvlip2  25987  dv11cn  25993  deg1ldg  26082  deg1leb  26085  plycpn  26280  vieta1lem2  26302  elqaa  26313  aalioulem2  26324  aaliou3lem3  26335  aaliou3lem4  26337  pserulm  26412  psercnlem2  26414  psercnlem1  26415  psercn  26416  abelth  26431  reeff1o  26437  pilem1  26441  efhalfpi  26460  coseq0negpitopi  26492  pige3ALT  26509  tanregt0  26528  efif1olem3  26533  efif1olem4  26534  efifo  26536  eff1olem  26537  efsubm  26540  logrn  26547  ellogrn  26548  relogf1o  26555  argregt0  26599  argrege0  26600  dvrelog  26626  dvloglem  26637  logf1o2  26639  dvlog  26640  efopnlem1  26645  efopnlem2  26646  logtayl  26649  cxpcn3lem  26736  cxpcn3  26737  resqrtcn  26738  asinneg  26875  asinrebnd  26890  atan0  26897  atanbnd  26915  areambl  26947  sqrtlim  26961  amgmlem  26978  lgamucov  27026  basellem1  27069  basellem4  27072  sqff1o  27170  dchrplusg  27235  bposlem6  27277  bposlem8  27279  dchrvmasumlem2  27486  pntibndlem1  27577  pntlemo  27595  qrng0  27609  ostth  27627  noextendseq  27656  bday0  27828  oldlim  27904  ons2ind  28292  zsex  28397  lmif  28878  islmib  28880  structiedg0val  29116  snstriedgval  29132  umgredgnlp  29241  usgrexmplef  29353  usgrexmpledg  29356  vtxdlfgrval  29579  upgr2pthnlp  29825  konigsberglem5  30351  ex-mod  30544  nowisdomv  30569  pliguhgr  30582  grporn  30617  ip0i  30921  ubthlem1  30966  ubthlem2  30967  axhcompl-zf  31094  normlem7  31212  bcseqi  31216  bcsiALT  31275  hlimf  31333  hlimuni  31334  hhssabloilem  31357  hhshsslem1  31363  hhsssh  31365  hhsscms  31374  occllem  31399  occl  31400  h1deoi  31645  h1dei  31646  h1de2ctlem  31651  h1de2ci  31652  spansni  31653  spanunsni  31675  pjpythi  31818  nmfn0  32083  nmopadjlem  32185  adjcoi  32196  nmopcoadji  32197  pjoccoi  32274  shatomistici  32457  iuninc  32656  imadifxp  32697  xppreima  32744  1stpreima  32806  2ndpreima  32807  fsuppcurry1  32823  fsuppcurry2  32824  hashgt1  32907  s3clhash  33034  gsummpt2d  33137  xrge0tsmsd  33161  tocyc01  33206  cyc3evpm  33238  cycpmconjslem2  33243  cyc3conja  33245  reofld  33433  rearchi  33436  nn0archi  33437  xrge0slmod  33438  elrspunidl  33518  dimval  33792  dimvalfi  33793  ply1degltdimlem  33813  algextdeglem8  33915  qtophaus  34027  iistmd  34093  xpinpreima  34097  xpinpreima2  34098  tpr2rico  34103  mndpluscn  34117  xrge0pluscn  34131  cnzh  34159  rezh  34160  qqhucn  34183  rrhcn  34188  cnrrext  34201  zrhre  34210  qqhre  34211  ismntop  34217  sigaex  34301  brsiga  34374  cntnevol  34419  voliune  34420  ddemeas  34427  1stmbfm  34451  2ndmbfm  34452  br2base  34460  dya2icoseg2  34469  dya2iocucvr  34475  carsgclctunlem2  34510  carsgclctunlem3  34511  sitgaddlemb  34539  eulerpartlemt  34562  eulerpartgbij  34563  eulerpartlemmf  34566  eulerpartlemgvv  34567  eulerpartlemgf  34570  eulerpart  34573  sseqmw  34582  sseqf  34583  sseqp1  34586  fiblem  34589  fibp1  34592  dstrvprob  34663  coinflipspace  34672  coinfliprv  34674  coinflippv  34675  ballotlem1  34678  ballotlem8  34728  circlemethhgt  34834  r11  35282  r12  35283  onvf1od  35342  usgrcyclgt2v  35366  iccllysconn  35485  rellysconn  35486  satf00  35609  fmla0  35617  msrid  35780  dfrdg2  36028  dfrdg4  36186  imagesset  36188  elhf  36409  filnetlem3  36615  limsucncmpi  36680  ttciunun  36746  bj-babygodel  36921  bj-idres  37527  taupilem3  37686  icoreresf  37721  icoreelrnab  37723  relowlssretop  37732  poimirlem3  37997  poimirlem9  38003  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem27  38021  poimirlem28  38022  poimirlem31  38025  poimirlem32  38026  mblfinlem1  38031  ovoliunnfl  38036  voliunnfl  38038  mbfresfi  38040  dvtan  38044  itg2addnc  38048  ftc1anclem3  38069  areacirc  38087  fdc  38119  ismrer1  38212  reheibor  38213  rngomndo  38309  gidsn  38326  ac6s6f  38547  cnvref4  38724  dfcnvrefrels2  38982  dfcnvrefrels3  38983  dedths  39461  tendo0co2  41287  erng1r  41494  dvalveclem  41524  dva0g  41526  dvh0g  41610  sn-it0e0  42900  sn-0tie0  42948  2rexfrabdioph  43248  3rexfrabdioph  43249  4rexfrabdioph  43250  6rexfrabdioph  43251  7rexfrabdioph  43252  rencldnfi  43273  jm2.27dlem2  43462  wepwso  43495  dfac11  43514  pwssplit4  43541  frlmpwfi  43550  isnumbasgrplem3  43557  mpaaeu  43602  proot1mul  43646  proot1hash  43647  epirron  43706  oneptr  43707  ordeldif1o  43712  oaomoencom  43769  oenassex  43770  cnvcnvintabd  44051  cnvrcl0  44076  dfrtrcl5  44080  cotrcltrcl  44176  frege92  44406  seff  44760  prmunb2  44762  binomcxplemdvbinom  44804  binomcxplemcvg  44805  binomcxplemnotnn0  44807  permac8prim  45465  sumsnd  45481  islptre  46071  stoweidlem34  46484  stoweidlem37  46487  stirlinglem11  46534  stirlinglem12  46535  stirlinglem13  46536  fouriersw  46681  natlocalincr  47328  nthrucw  47338  fundcmpsurbijinjpreimafv  47889  fundcmpsurinjimaid  47893  fmtnoinf  48021  gbowge7  48261  nnsum3primes4  48286  usgrexmpl12ngrlic  48537  gpgprismgr4cycllem2  48594  gpg5ngric  48626  2zrng0  48742  lmodn0  48993  zlmodzxzldeplem3  49000  lvecpsslmod  49005  0dig2pr01  49108  nelsubc3lem  49567  aacllem  50298  amgmwlem  50299