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  1630  nfcriOLD  2887  nfcriOLDOLD  2888  ceqsexv2d  3447  dtru  5248  intasym  5960  relcoi2  6120  funres11  6435  cnvresid  6437  omsindsOLD  7644  find  7652  fparlem1  7858  fparlem2  7859  dftpos4  7965  tposf12  7971  wfrlem14  8046  tfr2b  8110  tz7.44lem1  8119  xp01disjl  8201  xpcomco  8713  sbthlem2  8735  fidomdm  8931  brwdom2  9167  epnsym  9202  inf3lem6  9226  omex  9236  cnfcom  9293  trpredlem1  9310  trpredtr  9313  trpredmintr  9314  tz9.1c  9324  r1tr  9357  r1ord3g  9360  rankwflemb  9374  r1elwf  9377  r1elss  9387  rankval3b  9407  onssr1  9412  inlresf  9495  inrresf  9497  djuin  9499  infxpenlem  9592  alephnbtwn  9650  alephordilem1  9652  alephfp  9687  dfac13  9721  pwsdompw  9783  infdjuabs  9785  ackbij1  9817  ackbij2  9822  r1om  9823  cflim2  9842  fin23lem27  9907  fin23lem29  9920  fin23lem30  9921  fin1a2lem6  9984  fin1a2lem7  9985  fin1a2lem13  9991  itunitc1  9999  itunitc  10000  ituniiun  10001  hsmexlem5  10009  axcc2lem  10015  axcc3  10017  zorn2lem6  10080  zorn2lem7  10081  ttukeylem6  10093  axdc  10100  dmct  10103  iunfo  10118  cardval  10125  cardid  10126  pwcfsdom  10162  alephom  10164  canthp1lem2  10232  gchaleph2  10251  r1limwun  10315  inaprc  10415  nqerf  10509  recmulnq  10543  dmrecnq  10547  halfnq  10555  genpdm  10581  reclem3pr  10628  axresscn  10727  axpre-sup  10748  1re  10798  0re  10800  00id  10972  addid1  10977  0cnALT  11031  renegcli  11104  zexALT  12161  uzn0  12420  xrinfmss  12865  axdc4uzlem  13521  facnn  13806  fac0  13807  hashgval  13864  hashinf  13866  hashresfn  13871  hashrabrsn  13904  hashrabsn01  13905  hashrabsn1  13906  hashp1i  13935  hash1snb  13951  hashxplem  13965  fi1uzind  14028  cshw1  14352  cats1fv  14389  trclubgi  14525  cnrecnv  14693  rexanuz  14874  climdm  15080  lo1eq  15094  rlimeq  15095  sumsnf  15271  tanval  15652  rpnnen2lem11  15748  rpnnen  15751  sadadd2lem  15981  sadadd3  15983  sadaddlem  15988  sadasslem  15992  sadeq  15994  lcmgcdlem  16126  unbenlem  16424  prmreclem6  16437  vdwlem8  16504  vdwnnlem1  16511  0ram  16536  structcnvcnv  16680  prdsvallem  16913  prdsval  16914  prdsbas  16916  prdsplusg  16917  prdsmulr  16918  prdsvsca  16919  prdshom  16926  xpsfrn  17027  xpsff1o2  17028  catcoppccl  17577  catcoppcclOLD  17578  catcfuccl  17579  catcfucclOLD  17580  catcxpccl  17668  catcxpcclOLD  17669  tsrss  18049  gsumpropd2lem  18105  smndex2dnrinv  18296  mvdco  18791  efgmnvl  19058  efgval  19061  efgi0  19064  efgi1  19065  efgredeu  19096  0frgp  19123  abln0  19206  lt6abl  19234  gsumval3  19246  gsum2dlem2  19310  dprdres  19369  dmdprdsplit2lem  19386  ringn0  19575  isdrng2  19731  drngmcl  19734  drngid2  19737  cnfldplusf  20344  cnfldsub  20345  cnsubmlem  20365  cnsubglem  20366  cnmsubglem  20380  gzrngunitlem  20382  rge0srg  20388  zring0  20399  zzngim  20471  zrhpsgnmhm  20500  re0g  20528  pjfval  20622  pjpm  20624  psrplusg  20860  coe1sfi  21088  ply1plusgfvi  21117  marep01ma  21511  smadiadetlem1a  21514  smadiadetlem3lem2  21518  smadiadetlem3  21519  smadiadetlem4  21520  smadiadet  21521  indistpsALT  21864  tgrest  22010  leordtval2  22063  lmbr2  22110  cnprest  22140  lmff  22152  kgenidm  22398  tx1cn  22460  tx2cn  22461  elrnust  23076  ustbas  23079  psmetge0  23164  xmetge0  23196  qdensere  23621  cnblcld  23626  cnfldms  23627  cnfldtopn  23633  xrsdsre  23661  xrge0tsms  23685  iccpnfcnv  23795  xrhmeo  23797  cnheiborlem  23805  cnlmod  23991  lmmbr2  24110  lmcau  24164  metsscmetcld  24166  cncms  24206  cnfldcusp  24208  ovolctb  24341  ovoliunnul  24358  ismbl  24377  volf  24380  voliunlem1  24401  ioorf  24424  ioorinv  24427  ioorcl  24428  dyaddisj  24447  dyadmax  24449  dyadmbl  24451  mbfid  24486  ismbfd  24490  mbfimaopnlem  24506  limcresi  24736  dvreslem  24760  dvres2lem  24761  dvcjbr  24800  dvferm1  24836  dvferm2  24838  dvlip2  24846  dv11cn  24852  deg1ldg  24944  deg1leb  24947  plycpn  25136  vieta1lem2  25158  elqaa  25169  aalioulem2  25180  aaliou3lem3  25191  aaliou3lem4  25193  pserulm  25268  psercnlem2  25270  psercnlem1  25271  psercn  25272  abelth  25287  reeff1o  25293  pilem1  25297  efhalfpi  25315  coseq0negpitopi  25347  pige3ALT  25363  tanregt0  25382  efif1olem3  25387  efif1olem4  25388  efifo  25390  eff1olem  25391  efsubm  25394  logrn  25401  ellogrn  25402  relogf1o  25409  argregt0  25452  argrege0  25453  dvrelog  25479  dvloglem  25490  logf1o2  25492  dvlog  25493  efopnlem1  25498  efopnlem2  25499  logtayl  25502  cxpcn3lem  25587  cxpcn3  25588  resqrtcn  25589  asinneg  25723  asinrebnd  25738  atan0  25745  atanbnd  25763  areambl  25795  sqrtlim  25809  amgmlem  25826  lgamucov  25874  basellem1  25917  basellem4  25920  sqff1o  26018  dchrplusg  26082  bposlem6  26124  bposlem8  26126  dchrvmasumlem2  26333  mulog2sum  26372  pntibndlem1  26424  pntlemo  26442  qrng0  26456  ostth  26474  lmif  26830  islmib  26832  structiedg0val  27067  snstriedgval  27083  umgredgnlp  27192  usgrexmplef  27301  usgrexmpledg  27304  vtxdlfgrval  27527  upgr2pthnlp  27773  konigsberglem5  28293  ex-mod  28486  pliguhgr  28521  grporn  28556  ip0i  28860  ubthlem1  28905  ubthlem2  28906  axhcompl-zf  29033  normlem7  29151  bcseqi  29155  bcsiALT  29214  hlimf  29272  hlimuni  29273  hhssabloilem  29296  hhshsslem1  29302  hhsssh  29304  hhsscms  29313  occllem  29338  occl  29339  h1deoi  29584  h1dei  29585  h1de2ctlem  29590  h1de2ci  29591  spansni  29592  spanunsni  29614  pjpythi  29757  nmfn0  30022  nmopadjlem  30124  adjcoi  30135  nmopcoadji  30136  pjoccoi  30213  shatomistici  30396  iuninc  30573  imadifxp  30613  xppreima  30656  1stpreima  30713  2ndpreima  30714  fsuppcurry1  30734  fsuppcurry2  30735  hashgt1  30802  s3clhash  30896  gsummpt2d  30982  xrge0tsmsd  30990  tocyc01  31058  cyc3evpm  31090  cycpmconjslem2  31095  cyc3conja  31097  reofld  31212  rearchi  31214  nn0archi  31215  xrge0slmod  31216  elrspunidl  31274  dimval  31354  dimvalfi  31355  qtophaus  31454  iistmd  31520  xpinpreima  31524  xpinpreima2  31525  tpr2rico  31530  mndpluscn  31544  xrge0pluscn  31558  cnzh  31586  rezh  31587  qqhucn  31608  rrhcn  31613  cnrrext  31626  zrhre  31635  qqhre  31636  ismntop  31642  sigaex  31744  brsiga  31817  cntnevol  31862  voliune  31863  ddemeas  31870  1stmbfm  31893  2ndmbfm  31894  br2base  31902  dya2icoseg2  31911  dya2iocucvr  31917  carsgclctunlem2  31952  carsgclctunlem3  31953  sitgaddlemb  31981  eulerpartlemt  32004  eulerpartgbij  32005  eulerpartlemmf  32008  eulerpartlemgvv  32009  eulerpartlemgf  32012  eulerpart  32015  sseqmw  32024  sseqf  32025  sseqp1  32028  fiblem  32031  fibp1  32034  dstrvprob  32104  coinflipspace  32113  coinfliprv  32115  coinflippv  32116  ballotlem1  32119  ballotlem8  32169  circlemethhgt  32289  usgrcyclgt2v  32760  iccllysconn  32879  rellysconn  32880  satf00  33003  fmla0  33011  msrid  33174  dfrdg2  33441  on2recsfn  33512  on2recsov  33513  on2ind  33514  on3ind  33515  noextendseq  33556  bday0s  33708  oldlim  33755  dfrdg4  33939  imagesset  33941  elhf  34162  filnetlem3  34255  limsucncmpi  34320  bj-babygodel  34471  bj-idres  35015  taupilem3  35173  icoreresf  35209  icoreelrnab  35211  relowlssretop  35220  poimirlem3  35466  poimirlem9  35472  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem27  35490  poimirlem28  35491  poimirlem31  35494  poimirlem32  35495  mblfinlem1  35500  ovoliunnfl  35505  voliunnfl  35507  mbfresfi  35509  dvtan  35513  itg2addnc  35517  ftc1anclem3  35538  areacirc  35556  fdc  35589  ismrer1  35682  reheibor  35683  rngomndo  35779  gidsn  35796  ac6s6f  36017  eccnvepex  36156  dfcnvrefrels2  36330  dfcnvrefrels3  36331  dedths  36662  tendo0co2  38488  erng1r  38695  dvalveclem  38725  dva0g  38727  dvh0g  38811  sn-dtru  39851  sn-it0e0  40046  sn-0tie0  40070  2rexfrabdioph  40262  3rexfrabdioph  40263  4rexfrabdioph  40264  6rexfrabdioph  40265  7rexfrabdioph  40266  rencldnfi  40287  jm2.27dlem2  40476  wepwso  40512  dfac11  40531  pwssplit4  40558  frlmpwfi  40567  isnumbasgrplem3  40574  mpaaeu  40619  proot1mul  40668  proot1hash  40669  cnvcnvintabd  40825  cnvrcl0  40850  dfrtrcl5  40854  cotrcltrcl  40951  frege92  41181  seff  41541  prmunb2  41543  binomcxplemdvbinom  41585  binomcxplemcvg  41586  binomcxplemnotnn0  41588  sumsnd  42183  islptre  42778  stoweidlem34  43193  stoweidlem37  43196  stirlinglem11  43243  stirlinglem12  43244  stirlinglem13  43245  fouriersw  43390  fundcmpsurbijinjpreimafv  44475  fundcmpsurinjimaid  44479  fmtnoinf  44604  gbowge7  44831  nnsum3primes4  44856  2zrng0  45112  lmodn0  45452  zlmodzxzldeplem3  45459  lvecpsslmod  45464  0dig2pr01  45572  aacllem  46119  amgmwlem  46120