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  1626  nfcriOLD  2896  nfcriOLDOLD  2897  ceqsexv2d  3471  dtru  5288  intasym  6009  relcoi2  6169  funres11  6495  cnvresid  6497  omsindsOLD  7709  find  7717  fparlem1  7923  fparlem2  7924  dftpos4  8032  tposf12  8038  wfrlem14OLD  8124  tfr2b  8198  tz7.44lem1  8207  xp01disjl  8288  xpcomco  8802  sbthlem2  8824  fidomdm  9026  brwdom2  9262  epnsym  9297  inf3lem6  9321  omex  9331  cnfcom  9388  trpredlem1  9405  trpredtr  9408  trpredmintr  9409  tz9.1c  9419  r1tr  9465  r1ord3g  9468  rankwflemb  9482  r1elwf  9485  r1elss  9495  rankval3b  9515  onssr1  9520  inlresf  9603  inrresf  9605  djuin  9607  infxpenlem  9700  alephnbtwn  9758  alephordilem1  9760  alephfp  9795  dfac13  9829  pwsdompw  9891  infdjuabs  9893  ackbij1  9925  ackbij2  9930  r1om  9931  cflim2  9950  fin23lem27  10015  fin23lem29  10028  fin23lem30  10029  fin1a2lem6  10092  fin1a2lem7  10093  fin1a2lem13  10099  itunitc1  10107  itunitc  10108  ituniiun  10109  hsmexlem5  10117  axcc2lem  10123  axcc3  10125  zorn2lem6  10188  zorn2lem7  10189  ttukeylem6  10201  axdc  10208  dmct  10211  iunfo  10226  cardval  10233  cardid  10234  pwcfsdom  10270  alephom  10272  canthp1lem2  10340  gchaleph2  10359  r1limwun  10423  inaprc  10523  nqerf  10617  recmulnq  10651  dmrecnq  10655  halfnq  10663  genpdm  10689  reclem3pr  10736  axresscn  10835  axpre-sup  10856  1re  10906  0re  10908  00id  11080  addid1  11085  0cnALT  11139  renegcli  11212  zexALT  12269  uzn0  12528  xrinfmss  12973  axdc4uzlem  13631  facnn  13917  fac0  13918  hashgval  13975  hashinf  13977  hashresfn  13982  hashrabrsn  14015  hashrabsn01  14016  hashrabsn1  14017  hashp1i  14046  hash1snb  14062  hashxplem  14076  fi1uzind  14139  cshw1  14463  cats1fv  14500  trclubgi  14636  cnrecnv  14804  rexanuz  14985  climdm  15191  lo1eq  15205  rlimeq  15206  sumsnf  15383  tanval  15765  rpnnen2lem11  15861  rpnnen  15864  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  lcmgcdlem  16239  unbenlem  16537  prmreclem6  16550  vdwlem8  16617  vdwnnlem1  16624  0ram  16649  structcnvcnv  16782  prdsvallem  17082  prdsval  17083  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdshom  17095  xpsfrn  17196  xpsff1o2  17197  catcoppccl  17748  catcoppcclOLD  17749  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  tsrss  18222  gsumpropd2lem  18278  smndex2dnrinv  18469  mvdco  18968  efgmnvl  19235  efgval  19238  efgi0  19241  efgi1  19242  efgredeu  19273  0frgp  19300  abln0  19383  lt6abl  19411  gsumval3  19423  gsum2dlem2  19487  dprdres  19546  dmdprdsplit2lem  19563  ringn0  19757  isdrng2  19916  drngmcl  19919  drngid2  19922  cnfldplusf  20537  cnfldsub  20538  cnsubmlem  20558  cnsubglem  20559  cnmsubglem  20573  gzrngunitlem  20575  rge0srg  20581  zring0  20592  zzngim  20672  zrhpsgnmhm  20701  re0g  20729  pjfval  20823  pjpm  20825  psrplusg  21060  coe1sfi  21294  ply1plusgfvi  21323  marep01ma  21717  smadiadetlem1a  21720  smadiadetlem3lem2  21724  smadiadetlem3  21725  smadiadetlem4  21726  smadiadet  21727  indistpsALT  22071  indistpsALTOLD  22072  tgrest  22218  leordtval2  22271  lmbr2  22318  cnprest  22348  lmff  22360  kgenidm  22606  tx1cn  22668  tx2cn  22669  elrnust  23284  ustbas  23287  psmetge0  23373  xmetge0  23405  qdensere  23839  cnblcld  23844  cnfldms  23845  cnfldtopn  23851  xrsdsre  23879  xrge0tsms  23903  iccpnfcnv  24013  xrhmeo  24015  cnheiborlem  24023  cnlmod  24209  lmmbr2  24328  lmcau  24382  metsscmetcld  24384  cncms  24424  cnfldcusp  24426  ovolctb  24559  ovoliunnul  24576  ismbl  24595  volf  24598  voliunlem1  24619  ioorf  24642  ioorinv  24645  ioorcl  24646  dyaddisj  24665  dyadmax  24667  dyadmbl  24669  mbfid  24704  ismbfd  24708  mbfimaopnlem  24724  limcresi  24954  dvreslem  24978  dvres2lem  24979  dvcjbr  25018  dvferm1  25054  dvferm2  25056  dvlip2  25064  dv11cn  25070  deg1ldg  25162  deg1leb  25165  plycpn  25354  vieta1lem2  25376  elqaa  25387  aalioulem2  25398  aaliou3lem3  25409  aaliou3lem4  25411  pserulm  25486  psercnlem2  25488  psercnlem1  25489  psercn  25490  abelth  25505  reeff1o  25511  pilem1  25515  efhalfpi  25533  coseq0negpitopi  25565  pige3ALT  25581  tanregt0  25600  efif1olem3  25605  efif1olem4  25606  efifo  25608  eff1olem  25609  efsubm  25612  logrn  25619  ellogrn  25620  relogf1o  25627  argregt0  25670  argrege0  25671  dvrelog  25697  dvloglem  25708  logf1o2  25710  dvlog  25711  efopnlem1  25716  efopnlem2  25717  logtayl  25720  cxpcn3lem  25805  cxpcn3  25806  resqrtcn  25807  asinneg  25941  asinrebnd  25956  atan0  25963  atanbnd  25981  areambl  26013  sqrtlim  26027  amgmlem  26044  lgamucov  26092  basellem1  26135  basellem4  26138  sqff1o  26236  dchrplusg  26300  bposlem6  26342  bposlem8  26344  dchrvmasumlem2  26551  mulog2sum  26590  pntibndlem1  26642  pntlemo  26660  qrng0  26674  ostth  26692  lmif  27050  islmib  27052  structiedg0val  27295  snstriedgval  27311  umgredgnlp  27420  usgrexmplef  27529  usgrexmpledg  27532  vtxdlfgrval  27755  upgr2pthnlp  28001  konigsberglem5  28521  ex-mod  28714  pliguhgr  28749  grporn  28784  ip0i  29088  ubthlem1  29133  ubthlem2  29134  axhcompl-zf  29261  normlem7  29379  bcseqi  29383  bcsiALT  29442  hlimf  29500  hlimuni  29501  hhssabloilem  29524  hhshsslem1  29530  hhsssh  29532  hhsscms  29541  occllem  29566  occl  29567  h1deoi  29812  h1dei  29813  h1de2ctlem  29818  h1de2ci  29819  spansni  29820  spanunsni  29842  pjpythi  29985  nmfn0  30250  nmopadjlem  30352  adjcoi  30363  nmopcoadji  30364  pjoccoi  30441  shatomistici  30624  iuninc  30801  imadifxp  30841  xppreima  30884  1stpreima  30941  2ndpreima  30942  fsuppcurry1  30962  fsuppcurry2  30963  hashgt1  31030  s3clhash  31124  gsummpt2d  31211  xrge0tsmsd  31219  tocyc01  31287  cyc3evpm  31319  cycpmconjslem2  31324  cyc3conja  31326  reofld  31446  rearchi  31448  nn0archi  31449  xrge0slmod  31450  elrspunidl  31508  dimval  31588  dimvalfi  31589  qtophaus  31688  iistmd  31754  xpinpreima  31758  xpinpreima2  31759  tpr2rico  31764  mndpluscn  31778  xrge0pluscn  31792  cnzh  31820  rezh  31821  qqhucn  31842  rrhcn  31847  cnrrext  31860  zrhre  31869  qqhre  31870  ismntop  31876  sigaex  31978  brsiga  32051  cntnevol  32096  voliune  32097  ddemeas  32104  1stmbfm  32127  2ndmbfm  32128  br2base  32136  dya2icoseg2  32145  dya2iocucvr  32151  carsgclctunlem2  32186  carsgclctunlem3  32187  sitgaddlemb  32215  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemmf  32242  eulerpartlemgvv  32243  eulerpartlemgf  32246  eulerpart  32249  sseqmw  32258  sseqf  32259  sseqp1  32262  fiblem  32265  fibp1  32268  dstrvprob  32338  coinflipspace  32347  coinfliprv  32349  coinflippv  32350  ballotlem1  32353  ballotlem8  32403  circlemethhgt  32523  usgrcyclgt2v  32993  iccllysconn  33112  rellysconn  33113  satf00  33236  fmla0  33244  msrid  33407  dfrdg2  33677  ttrclco  33704  ttrclselem2  33712  on2recsfn  33753  on2recsov  33754  on2ind  33755  on3ind  33756  noextendseq  33797  bday0s  33949  oldlim  33996  dfrdg4  34180  imagesset  34182  elhf  34403  filnetlem3  34496  limsucncmpi  34561  bj-babygodel  34712  bj-idres  35258  taupilem3  35417  icoreresf  35450  icoreelrnab  35452  relowlssretop  35461  poimirlem3  35707  poimirlem9  35713  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem27  35731  poimirlem28  35732  poimirlem31  35735  poimirlem32  35736  mblfinlem1  35741  ovoliunnfl  35746  voliunnfl  35748  mbfresfi  35750  dvtan  35754  itg2addnc  35758  ftc1anclem3  35779  areacirc  35797  fdc  35830  ismrer1  35923  reheibor  35924  rngomndo  36020  gidsn  36037  ac6s6f  36258  eccnvepex  36397  dfcnvrefrels2  36571  dfcnvrefrels3  36572  dedths  36903  tendo0co2  38729  erng1r  38936  dvalveclem  38966  dva0g  38968  dvh0g  39052  sn-dtru  40116  sn-it0e0  40318  sn-0tie0  40342  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  rencldnfi  40559  jm2.27dlem2  40748  wepwso  40784  dfac11  40803  pwssplit4  40830  frlmpwfi  40839  isnumbasgrplem3  40846  mpaaeu  40891  proot1mul  40940  proot1hash  40941  cnvcnvintabd  41097  cnvrcl0  41122  dfrtrcl5  41126  cotrcltrcl  41222  frege92  41452  seff  41816  prmunb2  41818  binomcxplemdvbinom  41860  binomcxplemcvg  41861  binomcxplemnotnn0  41863  sumsnd  42458  islptre  43050  stoweidlem34  43465  stoweidlem37  43468  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  fouriersw  43662  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751  fmtnoinf  44876  gbowge7  45103  nnsum3primes4  45128  2zrng0  45384  lmodn0  45724  zlmodzxzldeplem3  45731  lvecpsslmod  45736  0dig2pr01  45844  aacllem  46391  amgmwlem  46392