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-sylsimp  1552  ceqsexv2d  3216  eqvinc  3300  dtru  4783  intasym  5430  relcoi2  5580  funres11  5880  cnvresid  5882  elnn  6967  omsinds  6976  fparlem1  7164  fparlem2  7165  dftpos4  7258  tposf12  7264  wfrlem14  7315  tfr2b  7379  tz7.44lem1  7388  xpcomco  7935  sbthlem2  7956  fidomdm  8128  hartogslem1  8330  brwdom2  8361  inf3lem6  8413  omex  8423  cnfcom  8480  tz9.1c  8489  r1tr  8522  r1ord3g  8525  rankwflemb  8539  r1elwf  8542  r1elss  8552  rankval3b  8572  onssr1  8577  infxpenlem  8719  alephnbtwn  8777  alephordilem1  8779  alephfp  8814  dfac13  8847  pwsdompw  8909  infcdaabs  8911  ackbij1  8943  ackbij2  8948  r1om  8949  cflim2  8968  fin23lem27  9033  fin23lem29  9046  fin23lem30  9047  fin1a2lem6  9110  fin1a2lem7  9111  fin1a2lem13  9117  itunitc1  9125  itunitc  9126  ituniiun  9127  hsmexlem5  9135  axcc2lem  9141  axcc3  9143  zorn2lem6  9206  zorn2lem7  9207  ttukeylem6  9219  axdc  9226  fodom  9227  iunfo  9240  cardval  9247  cardid  9248  pwcfsdom  9284  alephom  9286  canthp1lem2  9354  canthp1  9355  gchaleph2  9373  r1limwun  9437  inaprc  9537  nqerf  9631  recmulnq  9665  dmrecnq  9669  halfnq  9677  genpdm  9703  reclem3pr  9750  axresscn  9848  axpre-sup  9869  1re  9918  0re  9919  00id  10090  addid1  10095  renegcli  10221  zexALT  11273  uzn0  11579  dfle2  11856  xrinfmss  12012  xrge0neqmnf  12147  axdc4uzlem  12644  facnn  12924  fac0  12925  hashgval  12982  hashinf  12984  hashresfn  12990  hashrabrsn  13022  hashrabsn01  13023  hashrabsn1  13024  hashp1i  13052  hashxplem  13080  fi1uzind  13134  fi1uzindOLD  13140  cshw1  13419  cats1fv  13455  trclubgi  13585  trclubgiOLD  13586  cnrecnv  13753  rexanuz  13933  climdm  14133  lo1eq  14147  rlimeq  14148  sumsn  14319  tanval  14697  rpnnen2lem11  14792  rpnnen  14795  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  lcmgcdlem  15157  3prm  15244  unbenlem  15450  prmreclem6  15463  vdwlem8  15530  vdwnnlem1  15537  0ram  15562  structcnvcnv  15706  prdsval  15938  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  xpsfrn  16052  xpsff1o2  16054  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  tsrss  17046  gsumpropd2lem  17096  symgid  17644  mvdco  17688  efgmnvl  17950  efgval  17953  efgi0  17956  efgi1  17957  efgredeu  17988  0frgp  18015  abln0  18093  lt6abl  18119  gsumval3  18131  gsum2dlem2  18193  dprdres  18250  dmdprdsplit2lem  18267  ringn0  18426  isdrng2  18580  drngmcl  18583  drngid2  18586  psrplusg  19202  coe1sfi  19404  ply1plusgfvi  19433  cnfldplusf  19592  cnfldsub  19593  cnsubmlem  19613  cnmsubglem  19628  gzrngunitlem  19630  rge0srg  19636  zring0  19647  zzngim  19720  zrhpsgnmhm  19749  re0g  19777  pjfval  19869  pjpm  19871  marep01ma  20285  smadiadetlem1a  20288  smadiadetlem3lem2  20292  smadiadetlem3  20293  smadiadetlem4  20294  smadiadet  20295  indistpsALT  20627  tgrest  20773  leordtval2  20826  lmbr2  20873  cnprest  20903  lmff  20915  kgenidm  21160  tx1cn  21222  tx2cn  21223  hausdiag  21258  elrnust  21838  ustbas  21841  psmetge0  21927  xmetge0  21959  qdensere  22383  cnblcld  22388  cnfldms  22389  cnfldtopn  22395  xrsdsre  22421  xrge0tsms  22445  iccpnfcnv  22551  xrhmeo  22553  cnheiborlem  22561  cnlmod  22748  lmmbr2  22865  lmcau  22919  cmetss  22921  cncms  22959  cnfldcusp  22961  ovolctb  23065  ovoliunnul  23082  ismbl  23101  volf  23104  voliunlem1  23125  ioorf  23147  ioorinv  23150  ioorcl  23151  dyaddisj  23170  dyadmax  23172  dyadmbl  23174  mbfid  23209  ismbfd  23213  mbfimaopnlem  23228  limcresi  23455  dvreslem  23479  dvres2lem  23480  dvcjbr  23518  dvferm1  23552  dvferm2  23554  dvlip2  23562  dv11cn  23568  deg1ldg  23656  deg1leb  23659  plycpn  23848  vieta1lem2  23870  elqaa  23881  aalioulem2  23892  aaliou3lem3  23903  aaliou3lem4  23905  pserulm  23980  psercnlem2  23982  psercnlem1  23983  psercn  23984  abelth  23999  reeff1o  24005  pilem1  24009  efhalfpi  24027  coseq0negpitopi  24059  pige3  24073  tanregt0  24089  efif1olem3  24094  efif1olem4  24095  efifo  24097  eff1olem  24098  efsubm  24101  logrn  24109  ellogrn  24110  relogf1o  24117  argregt0  24160  argrege0  24161  dvrelog  24183  dvloglem  24194  logf1o2  24196  dvlog  24197  efopnlem1  24202  efopnlem2  24203  logtayl  24206  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  asinneg  24413  asinrebnd  24428  atan0  24435  atanbnd  24453  areambl  24485  sqrtlim  24499  amgmlem  24516  lgamucov  24564  basellem1  24607  basellem4  24610  sqff1o  24708  dchrplusg  24772  bposlem6  24814  bposlem8  24816  dchrvmasumlem2  24987  mulog2sum  25026  pntibndlem1  25078  pntlemo  25096  qrng0  25110  ostth  25128  lmif  25477  islmib  25479  structiedg0val  25699  snstriedgval  25713  umgredgnlp  25818  usgraexmplef  25929  usgraexmpledg  25932  constr1trl  26118  vdegp1ai  26511  ex-mod  26698  grporn  26759  ip0i  27064  ubthlem1  27110  ubthlem2  27111  axhcompl-zf  27239  normlem7  27357  bcseqi  27361  bcsiALT  27420  hlimf  27478  hlimuni  27479  hhssabloilem  27502  hhshsslem1  27508  hhsssh  27510  hhsscms  27520  occllem  27546  occl  27547  h1deoi  27792  h1dei  27793  h1de2ctlem  27798  h1de2ci  27799  spansni  27800  spanunsni  27822  pjpythi  27965  nmfn0  28230  nmopadjlem  28332  adjcoi  28343  nmopcoadji  28344  pjoccoi  28421  shatomistici  28604  imadifxp  28796  idssxp  28811  xppreima  28829  1stpreima  28867  2ndpreima  28868  dmct  28877  gsummpt2d  29112  xrge0tsmsd  29116  reofld  29171  rearchi  29173  nn0archi  29174  xrge0slmod  29175  qtophaus  29231  iistmd  29276  xpinpreima  29280  xpinpreima2  29281  tpr2rico  29286  mndpluscn  29300  xrge0pluscn  29314  cnzh  29342  rezh  29343  qqhucn  29364  rrhcn  29369  cnrrext  29382  zrhre  29391  qqhre  29392  ismntop  29398  sigaex  29499  brsiga  29573  cntnevol  29618  voliune  29619  ddemeas  29626  1stmbfm  29649  2ndmbfm  29650  br2base  29658  dya2icoseg2  29667  dya2iocucvr  29673  carsgclctunlem2  29708  carsgclctunlem3  29709  sitgaddlemb  29737  eulerpartlemt  29760  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpartlemgvv  29765  eulerpartlemgf  29768  eulerpart  29771  sseqmw  29780  sseqf  29781  sseqp1  29784  fiblem  29787  fibp1  29790  dstrvprob  29860  coinflipspace  29869  coinfliprv  29871  coinflippv  29872  ballotlem1  29875  ballotlem8  29925  iccllyscon  30486  rellyscon  30487  msrid  30696  dfrdg2  30945  trpredlem1  30971  trpredtr  30974  trpredmintr  30975  dfrdg4  31228  imagesset  31230  elhf  31451  filnetlem3  31545  limsucncmpi  31614  taupilem3  32342  icoreresf  32376  icoreelrnab  32378  relowlssretop  32387  poimirlem3  32582  poimirlem9  32588  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  mblfinlem1  32616  ovoliunnfl  32621  voliunnfl  32623  mbfresfi  32626  dvtan  32630  itg2addnc  32634  ftc1anclem3  32657  areacirc  32675  fdc  32711  ismrer1  32807  reheibor  32808  rngomndo  32904  gidsn  32921  ac6s6f  33151  elimhyps  33265  dedths  33266  tendo0co2  35094  erng1r  35301  dvalveclem  35332  dva0g  35334  dvh0g  35418  2rexfrabdioph  36378  3rexfrabdioph  36379  4rexfrabdioph  36380  6rexfrabdioph  36381  7rexfrabdioph  36382  rencldnfi  36403  jm2.27dlem2  36595  wepwso  36631  dfac11  36650  pwssplit4  36677  frlmpwfi  36686  isnumbasgrplem3  36694  mpaaeu  36739  proot1mul  36796  proot1hash  36797  cnvcnvintabd  36925  rtrclex  36943  cnvrcl0  36951  dfrtrcl5  36955  frege92  37269  seff  37530  prmunb2  37532  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  sumsnd  38208  sumsnf  38636  islptre  38686  stoweidlem34  38927  stoweidlem37  38930  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  fouriersw  39124  fmtnoinf  39986  gboge7  40185  nnsum3primes4  40204  usgrexmpledg  40486  vtxdlfgrval  40700  upgr2pthnlp  40938  konigsberglem5  41426  2zrng0  41728  lmodn0  42078  zlmodzxzldeplem3  42085  lvecpsslmod  42090  0dig2pr01  42202  aacllem  42356  amgmwlem  42357
  Copyright terms: Public domain W3C validator