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  1623  ceqsexv2d  3542  dtru  5271  intasym  5975  relcoi2  6128  funres11  6431  cnvresid  6433  elnn  7590  omsinds  7600  fparlem1  7807  fparlem2  7808  dftpos4  7911  tposf12  7917  wfrlem14  7968  tfr2b  8032  tz7.44lem1  8041  xp01disjl  8121  xpcomco  8607  sbthlem2  8628  fidomdm  8801  brwdom2  9037  epnsym  9072  inf3lem6  9096  omex  9106  cnfcom  9163  tz9.1c  9172  r1tr  9205  r1ord3g  9208  rankwflemb  9222  r1elwf  9225  r1elss  9235  rankval3b  9255  onssr1  9260  inlresf  9343  inrresf  9345  djuin  9347  infxpenlem  9439  alephnbtwn  9497  alephordilem1  9499  alephfp  9534  dfac13  9568  pwsdompw  9626  infdjuabs  9628  ackbij1  9660  ackbij2  9665  r1om  9666  cflim2  9685  fin23lem27  9750  fin23lem29  9763  fin23lem30  9764  fin1a2lem6  9827  fin1a2lem7  9828  fin1a2lem13  9834  itunitc1  9842  itunitc  9843  ituniiun  9844  hsmexlem5  9852  axcc2lem  9858  axcc3  9860  zorn2lem6  9923  zorn2lem7  9924  ttukeylem6  9936  axdc  9943  fodom  9944  dmct  9946  iunfo  9961  cardval  9968  cardid  9969  pwcfsdom  10005  alephom  10007  canthp1lem2  10075  gchaleph2  10094  r1limwun  10158  inaprc  10258  nqerf  10352  recmulnq  10386  dmrecnq  10390  halfnq  10398  genpdm  10424  reclem3pr  10471  axresscn  10570  axpre-sup  10591  1re  10641  0re  10643  00id  10815  addid1  10820  0cnALT  10874  renegcli  10947  zexALT  12002  uzn0  12261  xrinfmss  12704  axdc4uzlem  13352  facnn  13636  fac0  13637  hashgval  13694  hashinf  13696  hashresfn  13701  hashrabrsn  13734  hashrabsn01  13735  hashrabsn1  13736  hashp1i  13765  hash1snb  13781  hashxplem  13795  fi1uzind  13856  cshw1  14184  cats1fv  14221  trclubgi  14357  cnrecnv  14524  rexanuz  14705  climdm  14911  lo1eq  14925  rlimeq  14926  sumsnf  15099  tanval  15481  rpnnen2lem11  15577  rpnnen  15580  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  sadeq  15821  lcmgcdlem  15950  unbenlem  16244  prmreclem6  16257  vdwlem8  16324  vdwnnlem1  16331  0ram  16356  structcnvcnv  16497  prdsval  16728  prdsbas  16730  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  prdshom  16740  xpsfrn  16841  xpsff1o2  16842  catcoppccl  17368  catcfuccl  17369  catcxpccl  17457  tsrss  17833  gsumpropd2lem  17889  smndex2dnrinv  18080  mvdco  18573  efgmnvl  18840  efgval  18843  efgi0  18846  efgi1  18847  efgredeu  18878  0frgp  18905  abln0  18987  lt6abl  19015  gsumval3  19027  gsum2dlem2  19091  dprdres  19150  dmdprdsplit2lem  19167  ringn0  19353  isdrng2  19512  drngmcl  19515  drngid2  19518  psrplusg  20161  coe1sfi  20381  ply1plusgfvi  20410  cnfldplusf  20572  cnfldsub  20573  cnsubmlem  20593  cnsubglem  20594  cnmsubglem  20608  gzrngunitlem  20610  rge0srg  20616  zring0  20627  zzngim  20699  zrhpsgnmhm  20728  re0g  20756  pjfval  20850  pjpm  20852  marep01ma  21269  smadiadetlem1a  21272  smadiadetlem3lem2  21276  smadiadetlem3  21277  smadiadetlem4  21278  smadiadet  21279  indistpsALT  21621  tgrest  21767  leordtval2  21820  lmbr2  21867  cnprest  21897  lmff  21909  kgenidm  22155  tx1cn  22217  tx2cn  22218  elrnust  22833  ustbas  22836  psmetge0  22922  xmetge0  22954  qdensere  23378  cnblcld  23383  cnfldms  23384  cnfldtopn  23390  xrsdsre  23418  xrge0tsms  23442  iccpnfcnv  23548  xrhmeo  23550  cnheiborlem  23558  cnlmod  23744  lmmbr2  23862  lmcau  23916  metsscmetcld  23918  cncms  23958  cnfldcusp  23960  ovolctb  24091  ovoliunnul  24108  ismbl  24127  volf  24130  voliunlem1  24151  ioorf  24174  ioorinv  24177  ioorcl  24178  dyaddisj  24197  dyadmax  24199  dyadmbl  24201  mbfid  24236  ismbfd  24240  mbfimaopnlem  24256  limcresi  24483  dvreslem  24507  dvres2lem  24508  dvcjbr  24546  dvferm1  24582  dvferm2  24584  dvlip2  24592  dv11cn  24598  deg1ldg  24686  deg1leb  24689  plycpn  24878  vieta1lem2  24900  elqaa  24911  aalioulem2  24922  aaliou3lem3  24933  aaliou3lem4  24935  pserulm  25010  psercnlem2  25012  psercnlem1  25013  psercn  25014  abelth  25029  reeff1o  25035  pilem1  25039  efhalfpi  25057  coseq0negpitopi  25089  pige3ALT  25105  tanregt0  25123  efif1olem3  25128  efif1olem4  25129  efifo  25131  eff1olem  25132  efsubm  25135  logrn  25142  ellogrn  25143  relogf1o  25150  argregt0  25193  argrege0  25194  dvrelog  25220  dvloglem  25231  logf1o2  25233  dvlog  25234  efopnlem1  25239  efopnlem2  25240  logtayl  25243  cxpcn3lem  25328  cxpcn3  25329  resqrtcn  25330  asinneg  25464  asinrebnd  25479  atan0  25486  atanbnd  25504  areambl  25536  sqrtlim  25550  amgmlem  25567  lgamucov  25615  basellem1  25658  basellem4  25661  sqff1o  25759  dchrplusg  25823  bposlem6  25865  bposlem8  25867  dchrvmasumlem2  26074  mulog2sum  26113  pntibndlem1  26165  pntlemo  26183  qrng0  26197  ostth  26215  lmif  26571  islmib  26573  structiedg0val  26807  snstriedgval  26823  umgredgnlp  26932  usgrexmplef  27041  usgrexmpledg  27044  vtxdlfgrval  27267  upgr2pthnlp  27513  konigsberglem5  28035  ex-mod  28228  pliguhgr  28263  grporn  28298  ip0i  28602  ubthlem1  28647  ubthlem2  28648  axhcompl-zf  28775  normlem7  28893  bcseqi  28897  bcsiALT  28956  hlimf  29014  hlimuni  29015  hhssabloilem  29038  hhshsslem1  29044  hhsssh  29046  hhsscms  29055  occllem  29080  occl  29081  h1deoi  29326  h1dei  29327  h1de2ctlem  29332  h1de2ci  29333  spansni  29334  spanunsni  29356  pjpythi  29499  nmfn0  29764  nmopadjlem  29866  adjcoi  29877  nmopcoadji  29878  pjoccoi  29955  shatomistici  30138  iuninc  30312  imadifxp  30351  xppreima  30394  1stpreima  30442  2ndpreima  30443  fsuppcurry1  30461  fsuppcurry2  30462  hashgt1  30530  s3clhash  30624  gsummpt2d  30687  xrge0tsmsd  30692  tocyc01  30760  cyc3evpm  30792  cycpmconjslem2  30797  cyc3conja  30799  reofld  30913  rearchi  30915  nn0archi  30916  xrge0slmod  30917  dimval  31001  dimvalfi  31002  qtophaus  31100  iistmd  31145  xpinpreima  31149  xpinpreima2  31150  tpr2rico  31155  mndpluscn  31169  xrge0pluscn  31183  cnzh  31211  rezh  31212  qqhucn  31233  rrhcn  31238  cnrrext  31251  zrhre  31260  qqhre  31261  ismntop  31267  sigaex  31369  brsiga  31442  cntnevol  31487  voliune  31488  ddemeas  31495  1stmbfm  31518  2ndmbfm  31519  br2base  31527  dya2icoseg2  31536  dya2iocucvr  31542  carsgclctunlem2  31577  carsgclctunlem3  31578  sitgaddlemb  31606  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgf  31637  eulerpart  31640  sseqmw  31649  sseqf  31650  sseqp1  31653  fiblem  31656  fibp1  31659  dstrvprob  31729  coinflipspace  31738  coinfliprv  31740  coinflippv  31741  ballotlem1  31744  ballotlem8  31794  circlemethhgt  31914  usgrcyclgt2v  32378  iccllysconn  32497  rellysconn  32498  satf00  32621  fmla0  32629  msrid  32792  dfrdg2  33040  trpredlem1  33066  trpredtr  33069  trpredmintr  33070  noextendseq  33174  dfrdg4  33412  imagesset  33414  elhf  33635  filnetlem3  33728  limsucncmpi  33793  bj-babygodel  33937  bj-idres  34455  taupilem3  34603  icoreresf  34636  icoreelrnab  34638  relowlssretop  34647  poimirlem3  34910  poimirlem9  34916  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem27  34934  poimirlem28  34935  poimirlem31  34938  poimirlem32  34939  mblfinlem1  34944  ovoliunnfl  34949  voliunnfl  34951  mbfresfi  34953  dvtan  34957  itg2addnc  34961  ftc1anclem3  34984  areacirc  35002  fdc  35035  ismrer1  35131  reheibor  35132  rngomndo  35228  gidsn  35245  ac6s6f  35466  eccnvepex  35607  dfcnvrefrels2  35781  dfcnvrefrels3  35782  dedths  36113  tendo0co2  37939  erng1r  38146  dvalveclem  38176  dva0g  38178  dvh0g  38262  sn-dtru  39160  2rexfrabdioph  39442  3rexfrabdioph  39443  4rexfrabdioph  39444  6rexfrabdioph  39445  7rexfrabdioph  39446  rencldnfi  39467  jm2.27dlem2  39656  wepwso  39692  dfac11  39711  pwssplit4  39738  frlmpwfi  39747  isnumbasgrplem3  39754  mpaaeu  39799  proot1mul  39848  proot1hash  39849  cnvcnvintabd  40009  cnvrcl0  40034  dfrtrcl5  40038  cotrcltrcl  40119  frege92  40350  seff  40690  prmunb2  40692  binomcxplemdvbinom  40734  binomcxplemcvg  40735  binomcxplemnotnn0  40737  sumsnd  41332  islptre  41949  stoweidlem34  42368  stoweidlem37  42371  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  fouriersw  42565  fundcmpsurbijinjpreimafv  43616  fundcmpsurinjimaid  43620  fmtnoinf  43747  gbowge7  43977  nnsum3primes4  44002  2zrng0  44258  lmodn0  44599  zlmodzxzldeplem3  44606  lvecpsslmod  44611  0dig2pr01  44719  aacllem  44951  amgmwlem  44952