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  1614  ceqsexv2d  3543  dtru  5263  intasym  5969  relcoi2  6122  funres11  6425  cnvresid  6427  elnn  7578  omsinds  7588  fparlem1  7798  fparlem2  7799  dftpos4  7902  tposf12  7908  wfrlem14  7959  tfr2b  8023  tz7.44lem1  8032  xp01disjl  8112  xpcomco  8596  sbthlem2  8617  fidomdm  8790  brwdom2  9026  epnsym  9061  inf3lem6  9085  omex  9095  cnfcom  9152  tz9.1c  9161  r1tr  9194  r1ord3g  9197  rankwflemb  9211  r1elwf  9214  r1elss  9224  rankval3b  9244  onssr1  9249  inlresf  9332  inrresf  9334  djuin  9336  infxpenlem  9428  alephnbtwn  9486  alephordilem1  9488  alephfp  9523  dfac13  9557  pwsdompw  9615  infdjuabs  9617  ackbij1  9649  ackbij2  9654  r1om  9655  cflim2  9674  fin23lem27  9739  fin23lem29  9752  fin23lem30  9753  fin1a2lem6  9816  fin1a2lem7  9817  fin1a2lem13  9823  itunitc1  9831  itunitc  9832  ituniiun  9833  hsmexlem5  9841  axcc2lem  9847  axcc3  9849  zorn2lem6  9912  zorn2lem7  9913  ttukeylem6  9925  axdc  9932  fodom  9933  dmct  9935  iunfo  9950  cardval  9957  cardid  9958  pwcfsdom  9994  alephom  9996  canthp1lem2  10064  gchaleph2  10083  r1limwun  10147  inaprc  10247  nqerf  10341  recmulnq  10375  dmrecnq  10379  halfnq  10387  genpdm  10413  reclem3pr  10460  axresscn  10559  axpre-sup  10580  1re  10630  0re  10632  00id  10804  addid1  10809  0cnALT  10863  renegcli  10936  zexALT  11990  uzn0  12249  xrinfmss  12693  axdc4uzlem  13341  facnn  13625  fac0  13626  hashgval  13683  hashinf  13685  hashresfn  13690  hashrabrsn  13723  hashrabsn01  13724  hashrabsn1  13725  hashp1i  13754  hash1snb  13770  hashxplem  13784  fi1uzind  13845  cshw1  14174  cats1fv  14211  trclubgi  14347  cnrecnv  14514  rexanuz  14695  climdm  14901  lo1eq  14915  rlimeq  14916  sumsnf  15089  tanval  15471  rpnnen2lem11  15567  rpnnen  15570  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  lcmgcdlem  15940  unbenlem  16234  prmreclem6  16247  vdwlem8  16314  vdwnnlem1  16321  0ram  16346  structcnvcnv  16487  prdsval  16718  prdsbas  16720  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  prdshom  16730  xpsfrn  16831  xpsff1o2  16832  catcoppccl  17358  catcfuccl  17359  catcxpccl  17447  tsrss  17823  gsumpropd2lem  17879  symgid  18461  mvdco  18504  efgmnvl  18771  efgval  18774  efgi0  18777  efgi1  18778  efgredeu  18809  0frgp  18836  abln0  18918  lt6abl  18946  gsumval3  18958  gsum2dlem2  19022  dprdres  19081  dmdprdsplit2lem  19098  ringn0  19284  isdrng2  19443  drngmcl  19446  drngid2  19449  psrplusg  20091  coe1sfi  20311  ply1plusgfvi  20340  cnfldplusf  20502  cnfldsub  20503  cnsubmlem  20523  cnsubglem  20524  cnmsubglem  20538  gzrngunitlem  20540  rge0srg  20546  zring0  20557  zzngim  20629  zrhpsgnmhm  20658  re0g  20686  pjfval  20780  pjpm  20782  marep01ma  21199  smadiadetlem1a  21202  smadiadetlem3lem2  21206  smadiadetlem3  21207  smadiadetlem4  21208  smadiadet  21209  indistpsALT  21551  tgrest  21697  leordtval2  21750  lmbr2  21797  cnprest  21827  lmff  21839  kgenidm  22085  tx1cn  22147  tx2cn  22148  elrnust  22762  ustbas  22765  psmetge0  22851  xmetge0  22883  qdensere  23307  cnblcld  23312  cnfldms  23313  cnfldtopn  23319  xrsdsre  23347  xrge0tsms  23371  iccpnfcnv  23477  xrhmeo  23479  cnheiborlem  23487  cnlmod  23673  lmmbr2  23791  lmcau  23845  metsscmetcld  23847  cncms  23887  cnfldcusp  23889  ovolctb  24020  ovoliunnul  24037  ismbl  24056  volf  24059  voliunlem1  24080  ioorf  24103  ioorinv  24106  ioorcl  24107  dyaddisj  24126  dyadmax  24128  dyadmbl  24130  mbfid  24165  ismbfd  24169  mbfimaopnlem  24185  limcresi  24412  dvreslem  24436  dvres2lem  24437  dvcjbr  24475  dvferm1  24511  dvferm2  24513  dvlip2  24521  dv11cn  24527  deg1ldg  24615  deg1leb  24618  plycpn  24807  vieta1lem2  24829  elqaa  24840  aalioulem2  24851  aaliou3lem3  24862  aaliou3lem4  24864  pserulm  24939  psercnlem2  24941  psercnlem1  24942  psercn  24943  abelth  24958  reeff1o  24964  pilem1  24968  efhalfpi  24986  coseq0negpitopi  25018  pige3ALT  25034  tanregt0  25050  efif1olem3  25055  efif1olem4  25056  efifo  25058  eff1olem  25059  efsubm  25062  logrn  25069  ellogrn  25070  relogf1o  25077  argregt0  25120  argrege0  25121  dvrelog  25147  dvloglem  25158  logf1o2  25160  dvlog  25161  efopnlem1  25166  efopnlem2  25167  logtayl  25170  cxpcn3lem  25255  cxpcn3  25256  resqrtcn  25257  asinneg  25391  asinrebnd  25406  atan0  25413  atanbnd  25431  areambl  25464  sqrtlim  25478  amgmlem  25495  lgamucov  25543  basellem1  25586  basellem4  25589  sqff1o  25687  dchrplusg  25751  bposlem6  25793  bposlem8  25795  dchrvmasumlem2  26002  mulog2sum  26041  pntibndlem1  26093  pntlemo  26111  qrng0  26125  ostth  26143  lmif  26499  islmib  26501  structiedg0val  26735  snstriedgval  26751  umgredgnlp  26860  usgrexmplef  26969  usgrexmpledg  26972  vtxdlfgrval  27195  upgr2pthnlp  27441  konigsberglem5  27963  ex-mod  28156  pliguhgr  28191  grporn  28226  ip0i  28530  ubthlem1  28575  ubthlem2  28576  axhcompl-zf  28703  normlem7  28821  bcseqi  28825  bcsiALT  28884  hlimf  28942  hlimuni  28943  hhssabloilem  28966  hhshsslem1  28972  hhsssh  28974  hhsscms  28983  occllem  29008  occl  29009  h1deoi  29254  h1dei  29255  h1de2ctlem  29260  h1de2ci  29261  spansni  29262  spanunsni  29284  pjpythi  29427  nmfn0  29692  nmopadjlem  29794  adjcoi  29805  nmopcoadji  29806  pjoccoi  29883  shatomistici  30066  iuninc  30241  imadifxp  30280  xppreima  30323  1stpreima  30369  2ndpreima  30370  fsuppcurry1  30388  fsuppcurry2  30389  hashgt1  30457  s3clhash  30552  gsummpt2d  30615  xrge0tsmsd  30620  tocyc01  30688  cyc3evpm  30720  cycpmconjslem2  30725  cyc3conja  30727  reofld  30841  rearchi  30843  nn0archi  30844  xrge0slmod  30845  dimval  30901  dimvalfi  30902  qtophaus  31000  iistmd  31045  xpinpreima  31049  xpinpreima2  31050  tpr2rico  31055  mndpluscn  31069  xrge0pluscn  31083  cnzh  31111  rezh  31112  qqhucn  31133  rrhcn  31138  cnrrext  31151  zrhre  31160  qqhre  31161  ismntop  31167  sigaex  31269  brsiga  31342  cntnevol  31387  voliune  31388  ddemeas  31395  1stmbfm  31418  2ndmbfm  31419  br2base  31427  dya2icoseg2  31436  dya2iocucvr  31442  carsgclctunlem2  31477  carsgclctunlem3  31478  sitgaddlemb  31506  eulerpartlemt  31529  eulerpartgbij  31530  eulerpartlemmf  31533  eulerpartlemgvv  31534  eulerpartlemgf  31537  eulerpart  31540  sseqmw  31549  sseqf  31550  sseqp1  31553  fiblem  31556  fibp1  31559  dstrvprob  31629  coinflipspace  31638  coinfliprv  31640  coinflippv  31641  ballotlem1  31644  ballotlem8  31694  circlemethhgt  31814  usgrcyclgt2v  32276  iccllysconn  32395  rellysconn  32396  satf00  32519  fmla0  32527  msrid  32690  dfrdg2  32938  trpredlem1  32964  trpredtr  32967  trpredmintr  32968  noextendseq  33072  dfrdg4  33310  imagesset  33312  elhf  33533  filnetlem3  33626  limsucncmpi  33691  bj-babygodel  33835  bj-idres  34345  taupilem3  34483  icoreresf  34516  icoreelrnab  34518  relowlssretop  34527  poimirlem3  34777  poimirlem9  34783  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem27  34801  poimirlem28  34802  poimirlem31  34805  poimirlem32  34806  mblfinlem1  34811  ovoliunnfl  34816  voliunnfl  34818  mbfresfi  34820  dvtan  34824  itg2addnc  34828  ftc1anclem3  34851  areacirc  34869  fdc  34903  ismrer1  34999  reheibor  35000  rngomndo  35096  gidsn  35113  ac6s6f  35334  eccnvepex  35475  dfcnvrefrels2  35648  dfcnvrefrels3  35649  dedths  35980  tendo0co2  37806  erng1r  38013  dvalveclem  38043  dva0g  38045  dvh0g  38129  sn-dtru  38991  2rexfrabdioph  39273  3rexfrabdioph  39274  4rexfrabdioph  39275  6rexfrabdioph  39276  7rexfrabdioph  39277  rencldnfi  39298  jm2.27dlem2  39487  wepwso  39523  dfac11  39542  pwssplit4  39569  frlmpwfi  39578  isnumbasgrplem3  39585  mpaaeu  39630  proot1mul  39679  proot1hash  39680  cnvcnvintabd  39840  cnvrcl0  39865  dfrtrcl5  39869  cotrcltrcl  39950  frege92  40181  seff  40521  prmunb2  40523  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemnotnn0  40568  sumsnd  41163  islptre  41780  stoweidlem34  42200  stoweidlem37  42203  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  fouriersw  42397  fmtnoinf  43545  gbowge7  43775  nnsum3primes4  43800  smndex2dnrinv  43985  2zrng0  44107  lmodn0  44448  zlmodzxzldeplem3  44455  lvecpsslmod  44460  0dig2pr01  44568  aacllem  44800  amgmwlem  44801
  Copyright terms: Public domain W3C validator