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  1621  ceqsexv2dOLD  3518  dtruALT2  5352  dtruOLD  5428  intasym  6117  relcoi2  6279  funres11  6624  cnvresid  6626  find  7900  fparlem1  8120  fparlem2  8121  dftpos4  8253  tposf12  8259  wfrlem14OLD  8345  tfr2b  8419  tz7.44lem1  8428  ord3  8506  xp01disjl  8513  on2recsfn  8688  on2recsov  8689  on2ind  8690  on3ind  8691  xpcomco  9085  sbthlem2  9107  fidomdm  9357  brwdom2  9596  epnsym  9632  inf3lem6  9656  cnfcom  9723  ttrclco  9741  ttrclselem2  9749  tz9.1c  9753  frr1  9782  r1tr  9799  r1ord3g  9802  rankwflemb  9816  r1elwf  9819  r1elss  9829  rankval3b  9849  onssr1  9854  inlresf  9937  inrresf  9939  djuin  9941  infxpenlem  10036  alephnbtwn  10094  alephordilem1  10096  alephfp  10131  dfac13  10166  pwsdompw  10226  infdjuabs  10228  ackbij1  10260  ackbij2  10265  r1om  10266  cflim2  10286  fin23lem27  10351  fin23lem29  10364  fin23lem30  10365  fin1a2lem6  10428  fin1a2lem7  10429  fin1a2lem13  10435  itunitc1  10443  itunitc  10444  ituniiun  10445  hsmexlem5  10453  axcc2lem  10459  axcc3  10461  zorn2lem6  10524  zorn2lem7  10525  ttukeylem6  10537  dmct  10547  iunfo  10562  cardval  10569  cardid  10570  alephom  10608  canthp1lem2  10676  gchaleph2  10695  r1limwun  10759  inaprc  10859  nqerf  10953  recmulnq  10987  dmrecnq  10991  halfnq  10999  genpdm  11025  reclem3pr  11072  axresscn  11171  axpre-sup  11192  1re  11244  0re  11246  00id  11419  addrid  11424  0cnALT  11479  renegcli  11553  zexALT  12617  uzn0  12878  xrinfmss  13335  axdc4uzlem  14007  facnn  14297  fac0  14298  hashgval  14355  hashinf  14357  hashresfn  14362  hashrabrsn  14394  hashrabsn01  14395  hashrabsn1  14396  hashp1i  14425  hash1snb  14441  hashxplem  14455  fi1uzind  14529  cshw1  14843  cats1fv  14881  s7f1o  14988  trclubgi  15019  cnrecnv  15187  rexanuz  15367  climdm  15573  lo1eq  15587  rlimeq  15588  sumsnf  15762  tanval  16147  rpnnen2lem11  16243  rpnnen  16246  sadadd2lem  16479  sadadd3  16481  sadaddlem  16486  sadasslem  16490  sadeq  16492  lcmgcdlem  16626  unbenlem  16929  prmreclem6  16942  vdwlem8  17009  vdwnnlem1  17016  0ram  17041  structcnvcnv  17173  prdsvallem  17475  prdsval  17476  prdsbas  17478  prdsplusg  17479  prdsmulr  17480  prdsvsca  17481  prdshom  17488  xpsfrn  17589  xpsff1o2  17590  catcoppccl  18138  catcfuccl  18139  catcxpccl  18227  tsrss  18608  gsumpropd2lem  18666  smndex2dnrinv  18902  mvdco  19436  efgmnvl  19705  efgval  19708  efgi0  19711  efgi1  19712  efgredeu  19743  0frgp  19770  abln0  19858  lt6abl  19886  gsumval3  19898  gsum2dlem2  19962  dprdres  20021  dmdprdsplit2lem  20038  ringn0  20281  isdrng2  20716  drngmclOLD  20724  drngid2  20725  cnfldplusf  21376  cnfldsub  21377  cnsubmlem  21399  cnsubglem  21400  cnmsubglem  21415  gzrngunitlem  21417  rge0srg  21423  zring0  21436  pzriprnglem10  21468  zzngim  21538  zrhpsgnmhm  21569  re0g  21597  pjfval  21693  pjpm  21695  psrplusg  21923  coe1sfi  22182  ply1plusgfvi  22210  marep01ma  22633  smadiadetlem1a  22636  smadiadetlem3lem2  22640  smadiadetlem3  22641  smadiadetlem4  22642  smadiadet  22643  indistpsALT  22986  tgrest  23132  leordtval2  23185  lmbr2  23232  cnprest  23262  lmff  23274  kgenidm  23520  tx1cn  23582  tx2cn  23583  ustbas  24201  psmetge0  24286  xmetge0  24318  qdensere  24745  cnblcld  24750  cnfldms  24751  cnfldtopn  24757  xrsdsre  24787  xrge0tsms  24811  iccpnfcnv  24930  xrhmeo  24932  cnheiborlem  24941  cnlmod  25128  recvs  25134  lmmbr2  25248  lmcau  25302  metsscmetcld  25304  cncms  25344  cnfldcusp  25346  ovolctb  25480  ovoliunnul  25497  ismbl  25516  volf  25519  voliunlem1  25540  ioorf  25563  ioorinv  25566  ioorcl  25567  dyaddisj  25586  dyadmax  25588  dyadmbl  25590  mbfid  25625  ismbfd  25629  mbfimaopnlem  25645  limcresi  25875  dvreslem  25899  dvres2lem  25900  dvcjbr  25942  dvferm1  25978  dvferm2  25980  dvlip2  25989  dv11cn  25995  deg1ldg  26086  deg1leb  26089  plycpn  26286  vieta1lem2  26308  elqaa  26319  aalioulem2  26330  aaliou3lem3  26341  aaliou3lem4  26343  pserulm  26420  psercnlem2  26423  psercnlem1  26424  psercn  26425  abelth  26440  reeff1o  26446  pilem1  26450  efhalfpi  26468  coseq0negpitopi  26500  pige3ALT  26517  tanregt0  26536  efif1olem3  26541  efif1olem4  26542  efifo  26544  eff1olem  26545  efsubm  26548  logrn  26555  ellogrn  26556  relogf1o  26563  argregt0  26607  argrege0  26608  dvrelog  26634  dvloglem  26645  logf1o2  26647  dvlog  26648  efopnlem1  26653  efopnlem2  26654  logtayl  26657  cxpcn3lem  26745  cxpcn3  26746  resqrtcn  26747  asinneg  26884  asinrebnd  26899  atan0  26906  atanbnd  26924  areambl  26956  sqrtlim  26971  amgmlem  26988  lgamucov  27036  basellem1  27079  basellem4  27082  sqff1o  27180  dchrplusg  27246  bposlem6  27288  bposlem8  27290  dchrvmasumlem2  27497  pntibndlem1  27588  pntlemo  27606  qrng0  27620  ostth  27638  noextendseq  27667  bday0s  27828  oldlim  27880  zsex  28321  lmif  28748  islmib  28750  structiedg0val  28986  snstriedgval  29002  umgredgnlp  29111  usgrexmplef  29223  usgrexmpledg  29226  vtxdlfgrval  29450  upgr2pthnlp  29699  konigsberglem5  30222  ex-mod  30415  pliguhgr  30452  grporn  30487  ip0i  30791  ubthlem1  30836  ubthlem2  30837  axhcompl-zf  30964  normlem7  31082  bcseqi  31086  bcsiALT  31145  hlimf  31203  hlimuni  31204  hhssabloilem  31227  hhshsslem1  31233  hhsssh  31235  hhsscms  31244  occllem  31269  occl  31270  h1deoi  31515  h1dei  31516  h1de2ctlem  31521  h1de2ci  31522  spansni  31523  spanunsni  31545  pjpythi  31688  nmfn0  31953  nmopadjlem  32055  adjcoi  32066  nmopcoadji  32067  pjoccoi  32144  shatomistici  32327  iuninc  32520  imadifxp  32561  xppreima  32602  1stpreima  32663  2ndpreima  32664  fsuppcurry1  32683  fsuppcurry2  32684  hashgt1  32759  s3clhash  32879  gsummpt2d  32998  xrge0tsmsd  33011  tocyc01  33084  cyc3evpm  33116  cycpmconjslem2  33121  cyc3conja  33123  reofld  33313  rearchi  33315  nn0archi  33316  xrge0slmod  33317  elrspunidl  33397  dimval  33592  dimvalfi  33593  ply1degltdimlem  33614  algextdeglem8  33706  qtophaus  33776  iistmd  33842  xpinpreima  33846  xpinpreima2  33847  tpr2rico  33852  mndpluscn  33866  xrge0pluscn  33880  cnzh  33910  rezh  33911  qqhucn  33934  rrhcn  33939  cnrrext  33952  zrhre  33961  qqhre  33962  ismntop  33968  sigaex  34052  brsiga  34125  cntnevol  34170  voliune  34171  ddemeas  34178  1stmbfm  34203  2ndmbfm  34204  br2base  34212  dya2icoseg2  34221  dya2iocucvr  34227  carsgclctunlem2  34262  carsgclctunlem3  34263  sitgaddlemb  34291  eulerpartlemt  34314  eulerpartgbij  34315  eulerpartlemmf  34318  eulerpartlemgvv  34319  eulerpartlemgf  34322  eulerpart  34325  sseqmw  34334  sseqf  34335  sseqp1  34338  fiblem  34341  fibp1  34344  dstrvprob  34415  coinflipspace  34424  coinfliprv  34426  coinflippv  34427  ballotlem1  34430  ballotlem8  34480  circlemethhgt  34599  usgrcyclgt2v  35077  iccllysconn  35196  rellysconn  35197  satf00  35320  fmla0  35328  msrid  35491  dfrdg2  35737  dfrdg4  35893  imagesset  35895  elhf  36116  filnetlem3  36322  limsucncmpi  36387  bj-babygodel  36545  bj-idres  37102  taupilem3  37261  icoreresf  37294  icoreelrnab  37296  relowlssretop  37305  poimirlem3  37571  poimirlem9  37577  poimirlem15  37583  poimirlem16  37584  poimirlem17  37585  poimirlem19  37587  poimirlem27  37595  poimirlem28  37596  poimirlem31  37599  poimirlem32  37600  mblfinlem1  37605  ovoliunnfl  37610  voliunnfl  37612  mbfresfi  37614  dvtan  37618  itg2addnc  37622  ftc1anclem3  37643  areacirc  37661  fdc  37693  ismrer1  37786  reheibor  37787  rngomndo  37883  gidsn  37900  ac6s6f  38121  eccnvepex  38277  cnvref4  38292  dfcnvrefrels2  38470  dfcnvrefrels3  38471  dedths  38904  tendo0co2  40731  erng1r  40938  dvalveclem  40968  dva0g  40970  dvh0g  41054  sn-it0e0  42390  sn-0tie0  42414  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  rencldnfi  42777  jm2.27dlem2  42967  wepwso  43000  dfac11  43019  pwssplit4  43046  frlmpwfi  43055  isnumbasgrplem3  43062  mpaaeu  43107  proot1mul  43151  proot1hash  43152  epirron  43211  oneptr  43212  ordeldif1o  43218  oaomoencom  43275  oenassex  43276  cnvcnvintabd  43558  cnvrcl0  43583  dfrtrcl5  43587  cotrcltrcl  43683  frege92  43913  seff  44273  prmunb2  44275  binomcxplemdvbinom  44317  binomcxplemcvg  44318  binomcxplemnotnn0  44320  sumsnd  44976  islptre  45579  stoweidlem34  45994  stoweidlem37  45997  stirlinglem11  46044  stirlinglem12  46045  stirlinglem13  46046  fouriersw  46191  natlocalincr  46836  upwordsing  46844  fundcmpsurbijinjpreimafv  47340  fundcmpsurinjimaid  47344  fmtnoinf  47469  gbowge7  47696  nnsum3primes4  47721  usgrexmpl12ngrlic  47944  2zrng0  48106  lmodn0  48358  zlmodzxzldeplem3  48365  lvecpsslmod  48370  0dig2pr01  48477  aacllem  49316  amgmwlem  49317