MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2b Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mp2b.1 . . 3 𝜑
2 mp2b.2 . . 3 (𝜑𝜓)
31, 2ax-mp 5 . 2 𝜓
4 mp2b.3 . 2 (𝜓𝜒)
53, 4ax-mp 5 1 𝜒
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5
This theorem is referenced by:  minimp-syllsimp  1624  nfcriOLD  2895  nfcriOLDOLD  2896  ceqsexv2d  3495  dtruALT2  5323  dtruOLD  5396  intasym  6065  relcoi2  6225  funres11  6573  cnvresid  6575  omsindsOLD  7814  find  7823  fparlem1  8032  fparlem2  8033  dftpos4  8143  tposf12  8149  wfrlem14OLD  8235  tfr2b  8309  tz7.44lem1  8318  ord3  8396  xp01disjl  8405  xpcomco  8939  sbthlem2  8961  fidomdm  9206  brwdom2  9442  epnsym  9478  inf3lem6  9502  omex  9512  cnfcom  9569  ttrclco  9587  ttrclselem2  9595  tz9.1c  9599  frr1  9628  r1tr  9645  r1ord3g  9648  rankwflemb  9662  r1elwf  9665  r1elss  9675  rankval3b  9695  onssr1  9700  inlresf  9783  inrresf  9785  djuin  9787  infxpenlem  9882  alephnbtwn  9940  alephordilem1  9942  alephfp  9977  dfac13  10011  pwsdompw  10073  infdjuabs  10075  ackbij1  10107  ackbij2  10112  r1om  10113  cflim2  10132  fin23lem27  10197  fin23lem29  10210  fin23lem30  10211  fin1a2lem6  10274  fin1a2lem7  10275  fin1a2lem13  10281  itunitc1  10289  itunitc  10290  ituniiun  10291  hsmexlem5  10299  axcc2lem  10305  axcc3  10307  zorn2lem6  10370  zorn2lem7  10371  ttukeylem6  10383  axdc  10390  dmct  10393  iunfo  10408  cardval  10415  cardid  10416  pwcfsdom  10452  alephom  10454  canthp1lem2  10522  gchaleph2  10541  r1limwun  10605  inaprc  10705  nqerf  10799  recmulnq  10833  dmrecnq  10837  halfnq  10845  genpdm  10871  reclem3pr  10918  axresscn  11017  axpre-sup  11038  1re  11088  0re  11090  00id  11263  addid1  11268  0cnALT  11322  renegcli  11395  zexALT  12452  uzn0  12712  xrinfmss  13157  axdc4uzlem  13816  facnn  14102  fac0  14103  hashgval  14160  hashinf  14162  hashresfn  14167  hashrabrsn  14199  hashrabsn01  14200  hashrabsn1  14201  hashp1i  14230  hash1snb  14246  hashxplem  14260  fi1uzind  14323  cshw1  14641  cats1fv  14679  trclubgi  14815  cnrecnv  14983  rexanuz  15164  climdm  15370  lo1eq  15384  rlimeq  15385  sumsnf  15562  tanval  15944  rpnnen2lem11  16040  rpnnen  16043  sadadd2lem  16273  sadadd3  16275  sadaddlem  16280  sadasslem  16284  sadeq  16286  lcmgcdlem  16416  unbenlem  16714  prmreclem6  16727  vdwlem8  16794  vdwnnlem1  16801  0ram  16826  structcnvcnv  16959  prdsvallem  17270  prdsval  17271  prdsbas  17273  prdsplusg  17274  prdsmulr  17275  prdsvsca  17276  prdshom  17283  xpsfrn  17384  xpsff1o2  17385  catcoppccl  17937  catcoppcclOLD  17938  catcfuccl  17939  catcfucclOLD  17940  catcxpccl  18029  catcxpcclOLD  18030  tsrss  18412  gsumpropd2lem  18468  smndex2dnrinv  18659  mvdco  19159  efgmnvl  19425  efgval  19428  efgi0  19431  efgi1  19432  efgredeu  19463  0frgp  19490  abln0  19574  lt6abl  19601  gsumval3  19613  gsum2dlem2  19677  dprdres  19736  dmdprdsplit2lem  19753  ringn0  19950  isdrng2  20121  drngmcl  20124  drngid2  20127  cnfldplusf  20747  cnfldsub  20748  cnsubmlem  20768  cnsubglem  20769  cnmsubglem  20783  gzrngunitlem  20785  rge0srg  20791  zring0  20802  zzngim  20882  zrhpsgnmhm  20911  re0g  20939  pjfval  21035  pjpm  21037  psrplusg  21272  coe1sfi  21506  ply1plusgfvi  21535  marep01ma  21931  smadiadetlem1a  21934  smadiadetlem3lem2  21938  smadiadetlem3  21939  smadiadetlem4  21940  smadiadet  21941  indistpsALT  22285  indistpsALTOLD  22286  tgrest  22432  leordtval2  22485  lmbr2  22532  cnprest  22562  lmff  22574  kgenidm  22820  tx1cn  22882  tx2cn  22883  ustbas  23501  psmetge0  23587  xmetge0  23619  qdensere  24055  cnblcld  24060  cnfldms  24061  cnfldtopn  24067  xrsdsre  24095  xrge0tsms  24119  iccpnfcnv  24229  xrhmeo  24231  cnheiborlem  24239  cnlmod  24425  recvs  24431  lmmbr2  24545  lmcau  24599  metsscmetcld  24601  cncms  24641  cnfldcusp  24643  ovolctb  24776  ovoliunnul  24793  ismbl  24812  volf  24815  voliunlem1  24836  ioorf  24859  ioorinv  24862  ioorcl  24863  dyaddisj  24882  dyadmax  24884  dyadmbl  24886  mbfid  24921  ismbfd  24925  mbfimaopnlem  24941  limcresi  25171  dvreslem  25195  dvres2lem  25196  dvcjbr  25235  dvferm1  25271  dvferm2  25273  dvlip2  25281  dv11cn  25287  deg1ldg  25379  deg1leb  25382  plycpn  25571  vieta1lem2  25593  elqaa  25604  aalioulem2  25615  aaliou3lem3  25626  aaliou3lem4  25628  pserulm  25703  psercnlem2  25705  psercnlem1  25706  psercn  25707  abelth  25722  reeff1o  25728  pilem1  25732  efhalfpi  25750  coseq0negpitopi  25782  pige3ALT  25798  tanregt0  25817  efif1olem3  25822  efif1olem4  25823  efifo  25825  eff1olem  25826  efsubm  25829  logrn  25836  ellogrn  25837  relogf1o  25844  argregt0  25887  argrege0  25888  dvrelog  25914  dvloglem  25925  logf1o2  25927  dvlog  25928  efopnlem1  25933  efopnlem2  25934  logtayl  25937  cxpcn3lem  26022  cxpcn3  26023  resqrtcn  26024  asinneg  26158  asinrebnd  26173  atan0  26180  atanbnd  26198  areambl  26230  sqrtlim  26244  amgmlem  26261  lgamucov  26309  basellem1  26352  basellem4  26355  sqff1o  26453  dchrplusg  26517  bposlem6  26559  bposlem8  26561  dchrvmasumlem2  26768  mulog2sum  26807  pntibndlem1  26859  pntlemo  26877  qrng0  26891  ostth  26909  noextendseq  26937  bday0s  27089  oldlim  27136  lmif  27525  islmib  27527  structiedg0val  27771  snstriedgval  27787  umgredgnlp  27896  usgrexmplef  28005  usgrexmpledg  28008  vtxdlfgrval  28231  upgr2pthnlp  28478  konigsberglem5  28998  ex-mod  29191  pliguhgr  29226  grporn  29261  ip0i  29565  ubthlem1  29610  ubthlem2  29611  axhcompl-zf  29738  normlem7  29856  bcseqi  29860  bcsiALT  29919  hlimf  29977  hlimuni  29978  hhssabloilem  30001  hhshsslem1  30007  hhsssh  30009  hhsscms  30018  occllem  30043  occl  30044  h1deoi  30289  h1dei  30290  h1de2ctlem  30295  h1de2ci  30296  spansni  30297  spanunsni  30319  pjpythi  30462  nmfn0  30727  nmopadjlem  30829  adjcoi  30840  nmopcoadji  30841  pjoccoi  30918  shatomistici  31101  iuninc  31276  imadifxp  31316  xppreima  31359  1stpreima  31415  2ndpreima  31416  fsuppcurry1  31436  fsuppcurry2  31437  hashgt1  31504  s3clhash  31598  gsummpt2d  31685  xrge0tsmsd  31693  tocyc01  31761  cyc3evpm  31793  cycpmconjslem2  31798  cyc3conja  31800  reofld  31929  rearchi  31931  nn0archi  31932  xrge0slmod  31933  elrspunidl  31992  dimval  32083  dimvalfi  32084  qtophaus  32190  iistmd  32256  xpinpreima  32260  xpinpreima2  32261  tpr2rico  32266  mndpluscn  32280  xrge0pluscn  32294  cnzh  32324  rezh  32325  qqhucn  32346  rrhcn  32351  cnrrext  32364  zrhre  32373  qqhre  32374  ismntop  32380  sigaex  32482  brsiga  32555  cntnevol  32600  voliune  32601  ddemeas  32608  1stmbfm  32633  2ndmbfm  32634  br2base  32642  dya2icoseg2  32651  dya2iocucvr  32657  carsgclctunlem2  32692  carsgclctunlem3  32693  sitgaddlemb  32721  eulerpartlemt  32744  eulerpartgbij  32745  eulerpartlemmf  32748  eulerpartlemgvv  32749  eulerpartlemgf  32752  eulerpart  32755  sseqmw  32764  sseqf  32765  sseqp1  32768  fiblem  32771  fibp1  32774  dstrvprob  32844  coinflipspace  32853  coinfliprv  32855  coinflippv  32856  ballotlem1  32859  ballotlem8  32909  circlemethhgt  33029  usgrcyclgt2v  33498  iccllysconn  33617  rellysconn  33618  satf00  33741  fmla0  33749  msrid  33912  dfrdg2  34160  on2recsfn  34211  on2recsov  34212  on2ind  34213  on3ind  34214  dfrdg4  34431  imagesset  34433  elhf  34654  filnetlem3  34747  limsucncmpi  34812  bj-babygodel  34963  bj-idres  35526  taupilem3  35685  icoreresf  35718  icoreelrnab  35720  relowlssretop  35729  poimirlem3  35976  poimirlem9  35982  poimirlem15  35988  poimirlem16  35989  poimirlem17  35990  poimirlem19  35992  poimirlem27  36000  poimirlem28  36001  poimirlem31  36004  poimirlem32  36005  mblfinlem1  36010  ovoliunnfl  36015  voliunnfl  36017  mbfresfi  36019  dvtan  36023  itg2addnc  36027  ftc1anclem3  36048  areacirc  36066  fdc  36099  ismrer1  36192  reheibor  36193  rngomndo  36289  gidsn  36306  ac6s6f  36527  eccnvepex  36691  cnvref4  36706  dfcnvrefrels2  36885  dfcnvrefrels3  36886  dedths  37319  tendo0co2  39146  erng1r  39353  dvalveclem  39383  dva0g  39385  dvh0g  39469  sn-it0e0  40752  sn-0tie0  40776  2rexfrabdioph  40984  3rexfrabdioph  40985  4rexfrabdioph  40986  6rexfrabdioph  40987  7rexfrabdioph  40988  rencldnfi  41009  jm2.27dlem2  41199  wepwso  41235  dfac11  41254  pwssplit4  41281  frlmpwfi  41290  isnumbasgrplem3  41297  mpaaeu  41342  proot1mul  41391  proot1hash  41392  cnvcnvintabd  41634  cnvrcl0  41659  dfrtrcl5  41663  cotrcltrcl  41759  frege92  41989  seff  42353  prmunb2  42355  binomcxplemdvbinom  42397  binomcxplemcvg  42398  binomcxplemnotnn0  42400  sumsnd  42995  islptre  43613  stoweidlem34  44028  stoweidlem37  44031  stirlinglem11  44078  stirlinglem12  44079  stirlinglem13  44080  fouriersw  44225  natlocalincr  44864  upwordsing  44872  fundcmpsurbijinjpreimafv  45348  fundcmpsurinjimaid  45352  fmtnoinf  45477  gbowge7  45704  nnsum3primes4  45729  2zrng0  45985  lmodn0  46325  zlmodzxzldeplem3  46332  lvecpsslmod  46337  0dig2pr01  46445  aacllem  46993  amgmwlem  46994
  Copyright terms: Public domain W3C validator