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  1625  nfcriOLD  2896  nfcriOLDOLD  2897  ceqsexv2d  3496  dtruALT2  5324  dtruOLD  5397  intasym  6066  relcoi2  6226  funres11  6574  cnvresid  6576  omsindsOLD  7815  find  7824  fparlem1  8033  fparlem2  8034  dftpos4  8144  tposf12  8150  wfrlem14OLD  8236  tfr2b  8310  tz7.44lem1  8319  ord3  8397  xp01disjl  8406  xpcomco  8940  sbthlem2  8962  fidomdm  9207  brwdom2  9443  epnsym  9479  inf3lem6  9503  omex  9513  cnfcom  9570  ttrclco  9588  ttrclselem2  9596  tz9.1c  9600  frr1  9629  r1tr  9646  r1ord3g  9649  rankwflemb  9663  r1elwf  9666  r1elss  9676  rankval3b  9696  onssr1  9701  inlresf  9784  inrresf  9786  djuin  9788  infxpenlem  9883  alephnbtwn  9941  alephordilem1  9943  alephfp  9978  dfac13  10012  pwsdompw  10074  infdjuabs  10076  ackbij1  10108  ackbij2  10113  r1om  10114  cflim2  10133  fin23lem27  10198  fin23lem29  10211  fin23lem30  10212  fin1a2lem6  10275  fin1a2lem7  10276  fin1a2lem13  10282  itunitc1  10290  itunitc  10291  ituniiun  10292  hsmexlem5  10300  axcc2lem  10306  axcc3  10308  zorn2lem6  10371  zorn2lem7  10372  ttukeylem6  10384  axdc  10391  dmct  10394  iunfo  10409  cardval  10416  cardid  10417  pwcfsdom  10453  alephom  10455  canthp1lem2  10523  gchaleph2  10542  r1limwun  10606  inaprc  10706  nqerf  10800  recmulnq  10834  dmrecnq  10838  halfnq  10846  genpdm  10872  reclem3pr  10919  axresscn  11018  axpre-sup  11039  1re  11089  0re  11091  00id  11264  addid1  11269  0cnALT  11323  renegcli  11396  zexALT  12453  uzn0  12713  xrinfmss  13158  axdc4uzlem  13817  facnn  14103  fac0  14104  hashgval  14161  hashinf  14163  hashresfn  14168  hashrabrsn  14200  hashrabsn01  14201  hashrabsn1  14202  hashp1i  14231  hash1snb  14247  hashxplem  14261  fi1uzind  14324  cshw1  14642  cats1fv  14680  trclubgi  14816  cnrecnv  14984  rexanuz  15165  climdm  15371  lo1eq  15385  rlimeq  15386  sumsnf  15563  tanval  15945  rpnnen2lem11  16041  rpnnen  16044  sadadd2lem  16274  sadadd3  16276  sadaddlem  16281  sadasslem  16285  sadeq  16287  lcmgcdlem  16417  unbenlem  16715  prmreclem6  16728  vdwlem8  16795  vdwnnlem1  16802  0ram  16827  structcnvcnv  16960  prdsvallem  17271  prdsval  17272  prdsbas  17274  prdsplusg  17275  prdsmulr  17276  prdsvsca  17277  prdshom  17284  xpsfrn  17385  xpsff1o2  17386  catcoppccl  17938  catcoppcclOLD  17939  catcfuccl  17940  catcfucclOLD  17941  catcxpccl  18030  catcxpcclOLD  18031  tsrss  18413  gsumpropd2lem  18469  smndex2dnrinv  18660  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  27513  islmib  27515  structiedg0val  27759  snstriedgval  27775  umgredgnlp  27884  usgrexmplef  27993  usgrexmpledg  27996  vtxdlfgrval  28219  upgr2pthnlp  28466  konigsberglem5  28986  ex-mod  29179  pliguhgr  29214  grporn  29249  ip0i  29553  ubthlem1  29598  ubthlem2  29599  axhcompl-zf  29726  normlem7  29844  bcseqi  29848  bcsiALT  29907  hlimf  29965  hlimuni  29966  hhssabloilem  29989  hhshsslem1  29995  hhsssh  29997  hhsscms  30006  occllem  30031  occl  30032  h1deoi  30277  h1dei  30278  h1de2ctlem  30283  h1de2ci  30284  spansni  30285  spanunsni  30307  pjpythi  30450  nmfn0  30715  nmopadjlem  30817  adjcoi  30828  nmopcoadji  30829  pjoccoi  30906  shatomistici  31089  iuninc  31264  imadifxp  31304  xppreima  31347  1stpreima  31403  2ndpreima  31404  fsuppcurry1  31424  fsuppcurry2  31425  hashgt1  31492  s3clhash  31586  gsummpt2d  31673  xrge0tsmsd  31681  tocyc01  31749  cyc3evpm  31781  cycpmconjslem2  31786  cyc3conja  31788  reofld  31917  rearchi  31919  nn0archi  31920  xrge0slmod  31921  elrspunidl  31980  dimval  32071  dimvalfi  32072  qtophaus  32178  iistmd  32244  xpinpreima  32248  xpinpreima2  32249  tpr2rico  32254  mndpluscn  32268  xrge0pluscn  32282  cnzh  32312  rezh  32313  qqhucn  32334  rrhcn  32339  cnrrext  32352  zrhre  32361  qqhre  32362  ismntop  32368  sigaex  32470  brsiga  32543  cntnevol  32588  voliune  32589  ddemeas  32596  1stmbfm  32621  2ndmbfm  32622  br2base  32630  dya2icoseg2  32639  dya2iocucvr  32645  carsgclctunlem2  32680  carsgclctunlem3  32681  sitgaddlemb  32709  eulerpartlemt  32732  eulerpartgbij  32733  eulerpartlemmf  32736  eulerpartlemgvv  32737  eulerpartlemgf  32740  eulerpart  32743  sseqmw  32752  sseqf  32753  sseqp1  32756  fiblem  32759  fibp1  32762  dstrvprob  32832  coinflipspace  32841  coinfliprv  32843  coinflippv  32844  ballotlem1  32847  ballotlem8  32897  circlemethhgt  33017  usgrcyclgt2v  33486  iccllysconn  33605  rellysconn  33606  satf00  33729  fmla0  33737  msrid  33900  dfrdg2  34148  on2recsfn  34199  on2recsov  34200  on2ind  34201  on3ind  34202  dfrdg4  34422  imagesset  34424  elhf  34645  filnetlem3  34738  limsucncmpi  34803  bj-babygodel  34954  bj-idres  35517  taupilem3  35676  icoreresf  35709  icoreelrnab  35711  relowlssretop  35720  poimirlem3  35967  poimirlem9  35973  poimirlem15  35979  poimirlem16  35980  poimirlem17  35981  poimirlem19  35983  poimirlem27  35991  poimirlem28  35992  poimirlem31  35995  poimirlem32  35996  mblfinlem1  36001  ovoliunnfl  36006  voliunnfl  36008  mbfresfi  36010  dvtan  36014  itg2addnc  36018  ftc1anclem3  36039  areacirc  36057  fdc  36090  ismrer1  36183  reheibor  36184  rngomndo  36280  gidsn  36297  ac6s6f  36518  eccnvepex  36682  cnvref4  36697  dfcnvrefrels2  36876  dfcnvrefrels3  36877  dedths  37310  tendo0co2  39137  erng1r  39344  dvalveclem  39374  dva0g  39376  dvh0g  39460  sn-it0e0  40730  sn-0tie0  40754  2rexfrabdioph  40953  3rexfrabdioph  40954  4rexfrabdioph  40955  6rexfrabdioph  40956  7rexfrabdioph  40957  rencldnfi  40978  jm2.27dlem2  41168  wepwso  41204  dfac11  41223  pwssplit4  41250  frlmpwfi  41259  isnumbasgrplem3  41266  mpaaeu  41311  proot1mul  41360  proot1hash  41361  cnvcnvintabd  41603  cnvrcl0  41628  dfrtrcl5  41632  cotrcltrcl  41728  frege92  41958  seff  42322  prmunb2  42324  binomcxplemdvbinom  42366  binomcxplemcvg  42367  binomcxplemnotnn0  42369  sumsnd  42964  islptre  43582  stoweidlem34  43997  stoweidlem37  44000  stirlinglem11  44047  stirlinglem12  44048  stirlinglem13  44049  fouriersw  44194  natlocalincr  44833  upwordsing  44841  fundcmpsurbijinjpreimafv  45317  fundcmpsurinjimaid  45321  fmtnoinf  45446  gbowge7  45673  nnsum3primes4  45698  2zrng0  45954  lmodn0  46294  zlmodzxzldeplem3  46301  lvecpsslmod  46306  0dig2pr01  46414  aacllem  46962  amgmwlem  46963
  Copyright terms: Public domain W3C validator