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 ⊢ 𝜒

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5

This theorem is used by:  minimp-syllsimp  1655  dtruALT2  5339  intasym  6113  relcoi2  6279  funres11  6614  cnvresid  6616  find  7896  fparlem1  8113  fparlem2  8114  dftpos4  8247  tposf12  8253  tfr2b  8389  tz7.44lem1  8398  ord3  8475  xp01disjl  8483  on2recsfn  8659  on2recsov  8660  on2ind  8661  on3ind  8662  xpcomco  9069  sbthlem2  9090  fidomdm  9305  brwdom2  9549  epnsym  9592  inf3lem6  9616  cnfcom  9683  ttrclco  9701  ttrclselem2  9709  tz9.1c  9713  frr1  9745  r1tr  9762  r1ord3g  9765  rankwflemb  9779  r1elwf  9782  r1elss  9792  rankval3b  9812  onssr1  9817  inlresf  9923  inrresf  9925  djuin  9927  infxpenlem  10020  alephnbtwn  10078  alephordilem1  10080  alephfp  10115  dfac13  10149  pwsdompw  10209  infdjuabs  10211  ackbij1  10243  ackbij2  10248  r1om  10249  cflim2  10269  fin23lem27  10334  fin23lem29  10347  fin23lem30  10348  fin1a2lem6  10411  fin1a2lem7  10412  fin1a2lem13  10418  itunitc1  10426  itunitc  10427  ituniiun  10428  hsmexlem5  10436  axcc2lem  10442  axcc3  10444  zorn2lem6  10507  zorn2lem7  10508  ttukeylem6  10520  dmct  10530  dmctOLD  10531  iunfo  10551  cardval  10558  cardid  10559  alephom  10598  canthp1lem2  10666  gchaleph2  10685  r1limwun  10749  inaprc  10849  nqerf  10943  recmulnq  10977  dmrecnq  10981  halfnq  10989  genpdm  11015  reclem3pr  11062  axresscn  11161  axpre-sup  11182  1re  11236  0re  11238  00id  11413  addrid  11418  0cnALT  11473  renegcli  11547  zexALT  12639  uzn0  12908  xrinfmss  13366  axdc4uzlem  14051  facnn  14343  fac0  14344  hashgval  14401  hashinf  14403  hashresfn  14408  hashrabrsn  14440  hashrabsn01  14441  hashrabsn1  14442  hashp1i  14471  hash1snb  14488  hashxplem  14502  fi1uzind  14576  cshw1  14897  cats1fv  14934  s7f1o  15043  trclubgi  15074  cnrecnv  15256  rexanuz  15437  climdm  15645  lo1eq  15659  rlimeq  15660  sumsnf  15833  tanval  16222  rpnnen2lem11  16318  rpnnen  16321  sadadd2lem  16555  sadadd3  16557  sadaddlem  16562  sadasslem  16566  sadeq  16568  lcmgcdlem  16702  unbenlem  17006  prmreclem6  17019  vdwlem8  17086  vdwnnlem1  17093  0ram  17118  structcnvcnv  17251  prdsvallem  17545  prdsval  17546  prdsbas  17548  prdsplusg  17549  prdsmulr  17550  prdsvsca  17551  prdshom  17558  xpsfrn  17660  xpsff1o2  17661  catcoppccl  18212  catcfuccl  18213  catcxpccl  18301  tsrss  18683  gsumpropd2lem  18787  smndex2dnrinv  19033  mvdco  19578  efgmnvl  19847  efgval  19850  efgi0  19853  efgi1  19854  efgredeu  19885  0frgp  19912  abln0  20000  lt6abl  20028  gsumval3  20040  gsum2dlem2  20104  dprdres  20163  dmdprdsplit2lem  20180  ringn0  20459  isdrng2  20912  drngid2  20925  cnfldplusf  21618  cnfldsub  21619  cnsubmlem  21634  cnsubglem  21635  cnmsubglem  21649  gzrngunitlem  21651  rge0srg  21657  zring0  21677  pzriprnglem10  21709  zzngim  21771  zrhpsgnmhm  21803  re0g  21831  pjfval  21925  pjpm  21927  psrplusg  22158  coe1sfi  22444  ply1plusgfvi  22472  marep01ma  22888  smadiadetlem1a  22891  smadiadetlem3lem2  22895  smadiadetlem3  22896  smadiadetlem4  22897  smadiadet  22898  indistpsALT  23244  tgrest  23390  leordtval2  23443  lmbr2  23490  cnprest  23520  lmff  23532  kgenidm  23779  tx1cn  23841  tx2cn  23842  ustbas  24459  psmetge0  24544  xmetge0  24576  qdensere  25001  cnblcld  25006  cnfldms  25007  cnfldtopn  25013  xrsdsre  25043  xrge0tsms  25067  iccpnfcnv  25178  xrhmeo  25180  cnheiborlem  25188  cnlmod  25374  recvs  25380  lmmbr2  25493  lmcau  25547  metsscmetcld  25549  cncms  25589  cnfldcusp  25591  ovolctb  25724  ovoliunnul  25741  ismbl  25760  volf  25763  voliunlem1  25784  ioorf  25807  ioorinv  25810  ioorcl  25811  dyaddisj  25830  dyadmax  25832  dyadmbl  25834  mbfid  25869  ismbfd  25873  mbfimaopnlem  25889  limcresi  26119  dvreslem  26143  dvres2lem  26144  dvcjbr  26183  dvferm1  26219  dvferm2  26221  dvlip2  26229  dv11cn  26235  deg1ldg  26324  deg1leb  26327  plycpn  26526  vieta1lem2  26550  elqaa  26561  aalioulem2  26576  aaliou3lem3  26587  aaliou3lem4  26589  pserulm  26665  psercnlem2  26667  psercnlem1  26668  psercn  26669  abelth  26684  reeff1o  26690  pilem1  26694  efhalfpi  26716  coseq0negpitopi  26748  pige3ALT  26765  tanregt0  26784  efif1olem3  26789  efif1olem4  26790  efifo  26792  eff1olem  26793  efsubm  26796  logrn  26803  ellogrn  26804  relogf1o  26811  argregt0  26855  argrege0  26856  dvrelog  26882  dvloglem  26893  logf1o2  26895  dvlog  26896  efopnlem1  26901  efopnlem2  26902  logtayl  26905  cxpcn3lem  26992  cxpcn3  26993  resqrtcn  26994  asinneg  27131  asinrebnd  27146  atan0  27153  atanbnd  27171  areambl  27203  sqrtlim  27217  amgmlem  27234  lgamucov  27282  basellem1  27325  basellem4  27328  sqff1o  27426  dchrplusg  27491  bposlem6  27533  bposlem8  27535  dchrvmasumlem2  27742  pntibndlem1  27833  pntlemo  27851  qrng0  27865  ostth  27883  noextendseq  27911  bday0  28084  oldlim  28160  ons2ind  28548  zsex  28653  lmif  29177  islmib  29179  structiedg0val  29487  snstriedgval  29503  umgredgnlp  29612  usgrexmplef  29727  usgrexmpledg  29730  vtxdlfgrval  29953  upgr2pthnlp  30205  konigsberglem5  30744  ex-mod  30937  nowisdomv  30962  pliguhgr  30975  grporn  31010  ip0i  31314  ubthlem1  31359  ubthlem2  31360  axhcompl-zf  31487  normlem7  31605  bcseqi  31609  bcsiALT  31668  hlimf  31726  hlimuni  31727  hhssabloilem  31750  hhshsslem1  31756  hhsssh  31758  hhsscms  31767  occllem  31792  occl  31793  h1deoi  32038  h1dei  32039  h1de2ctlem  32044  h1de2ci  32045  spansni  32046  spanunsni  32068  pjpythi  32211  nmfn0  32476  nmopadjlem  32578  adjcoi  32589  nmopcoadji  32590  pjoccoi  32667  shatomistici  32850  iuninc  33042  imadifxp  33082  xppreima  33126  1stpreima  33187  2ndpreima  33188  fsuppcurry1  33203  fsuppcurry2  33204  hashgt1  33287  s3clhash  33399  gsummpt2d  33497  xrge0tsmsd  33521  tocyc01  33566  cyc3evpm  33598  cycpmconjslem2  33603  cyc3conja  33605  reofld  33791  rearchi  33794  nn0archi  33795  xrge0slmod  33796  elrspunidl  33864  dimval  34119  dimvalfi  34120  ply1degltdimlem  34140  algextdeglem8  34242  qtophaus  34354  iistmd  34420  xpinpreima  34424  xpinpreima2  34425  tpr2rico  34430  mndpluscn  34444  xrge0pluscn  34458  cnzh  34486  rezh  34487  qqhucn  34510  rrhcn  34515  cnrrext  34528  zrhre  34537  qqhre  34538  ismntop  34544  sigaex  34628  brsiga  34702  cntnevol  34747  voliune  34748  ddemeas  34755  1stmbfm  34779  2ndmbfm  34780  br2base  34788  dya2icoseg2  34797  dya2iocucvr  34803  carsgclctunlem2  34838  carsgclctunlem3  34839  sitgaddlemb  34867  eulerpartlemt  34890  eulerpartgbij  34891  eulerpartlemmf  34894  eulerpartlemgvv  34895  eulerpartlemgf  34898  eulerpart  34901  sseqmw  34910  sseqf  34911  sseqp1  34914  fiblem  34917  fibp1  34920  dstrvprob  34991  coinflipspace  35000  coinfliprv  35002  coinflippv  35003  ballotlem1  35006  ballotlem8  35056  circlemethhgt  35159  r11  35609  r12  35610  onvf1od  35712  usgrcyclgt2v  35732  iccllysconn  35837  rellysconn  35838  satf00  35961  fmla0  35969  msrid  36132  dfrdg2  36380  dfrdg4  36538  imagesset  36540  elhf  36762  filnetlem3  37007  limsucncmpi  37072  ttciunun  37138  bj-babygodel  37312  bj-idres  37920  taupilem3  38079  icoreresf  38114  icoreelrnab  38116  relowlssretop  38125  poimirlem3  38380  poimirlem9  38386  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem27  38404  poimirlem28  38405  poimirlem31  38408  poimirlem32  38409  mblfinlem1  38414  ovoliunnfl  38419  voliunnfl  38421  mbfresfi  38423  dvtan  38427  itg2addnc  38431  ftc1anclem3  38452  areacirc  38470  fdc  38503  ismrer1  38596  reheibor  38597  rngomndo  38693  gidsn  38710  ac6s6f  38929  cnvref4  39106  dfcnvrefrels2  39364  dfcnvrefrels3  39365  dedths  39843  tendo0co2  41669  erng1r  41876  dvalveclem  41906  dva0g  41908  dvh0g  41992  sn-it0e0  43299  sn-0tie0  43347  2rexfrabdioph  43645  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  rencldnfi  43670  jm2.27dlem2  43859  wepwso  43892  dfac11  43911  pwssplit4  43938  frlmpwfi  43947  isnumbasgrplem3  43954  mpaaeu  43999  proot1mul  44043  proot1hash  44044  epirron  44103  oneptr  44104  ordeldif1o  44109  oaomoencom  44166  oenassex  44167  cnvcnvintabd  44448  cnvrcl0  44473  dfrtrcl5  44477  cotrcltrcl  44573  frege92  44803  seff  45141  prmunb2  45143  binomcxplemdvbinom  45185  binomcxplemcvg  45186  binomcxplemnotnn0  45188  permac8prim  45845  sumsnd  45868  islptre  46457  stoweidlem34  46870  stoweidlem37  46873  stirlinglem11  46920  stirlinglem12  46921  stirlinglem13  46922  fouriersw  47067  fundcmpsurbijinjpreimafv  48315  fundcmpsurinjimaid  48319  fmtnoinf  48447  gbowge7  48687  nnsum3primes4  48712  usgrexmpl12ngrlic  48963  gpgprismgr4cycllem2  49020  gpg5ngric  49052  2zrng0  49167  lmodn0  49433  zlmodzxzldeplem3  49440  lvecpsslmod  49445  0dig2pr01  49548  nelsubc3lem  50004  aacllem  50780  amgmwlem  50828