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  2949  nfcriOLDOLD  2950  ceqsexv2d  3493  dtru  5239  intasym  5946  relcoi2  6100  funres11  6405  cnvresid  6407  elnn  7574  omsinds  7584  find  7591  fparlem1  7794  fparlem2  7795  dftpos4  7898  tposf12  7904  wfrlem14  7955  tfr2b  8019  tz7.44lem1  8028  xp01disjl  8108  xpcomco  8594  sbthlem2  8616  fidomdm  8789  brwdom2  9025  epnsym  9060  inf3lem6  9084  omex  9094  cnfcom  9151  tz9.1c  9160  r1tr  9193  r1ord3g  9196  rankwflemb  9210  r1elwf  9213  r1elss  9223  rankval3b  9243  onssr1  9248  inlresf  9331  inrresf  9333  djuin  9335  infxpenlem  9428  alephnbtwn  9486  alephordilem1  9488  alephfp  9523  dfac13  9557  pwsdompw  9619  infdjuabs  9621  ackbij1  9653  ackbij2  9658  r1om  9659  cflim2  9678  fin23lem27  9743  fin23lem29  9756  fin23lem30  9757  fin1a2lem6  9820  fin1a2lem7  9821  fin1a2lem13  9827  itunitc1  9835  itunitc  9836  ituniiun  9837  hsmexlem5  9845  axcc2lem  9851  axcc3  9853  zorn2lem6  9916  zorn2lem7  9917  ttukeylem6  9929  axdc  9936  dmct  9939  iunfo  9954  cardval  9961  cardid  9962  pwcfsdom  9998  alephom  10000  canthp1lem2  10068  gchaleph2  10087  r1limwun  10151  inaprc  10251  nqerf  10345  recmulnq  10379  dmrecnq  10383  halfnq  10391  genpdm  10417  reclem3pr  10464  axresscn  10563  axpre-sup  10584  1re  10634  0re  10636  00id  10808  addid1  10813  0cnALT  10867  renegcli  10940  zexALT  11993  uzn0  12252  xrinfmss  12695  axdc4uzlem  13350  facnn  13635  fac0  13636  hashgval  13693  hashinf  13695  hashresfn  13700  hashrabrsn  13733  hashrabsn01  13734  hashrabsn1  13735  hashp1i  13764  hash1snb  13780  hashxplem  13794  fi1uzind  13855  cshw1  14179  cats1fv  14216  trclubgi  14352  cnrecnv  14519  rexanuz  14700  climdm  14906  lo1eq  14920  rlimeq  14921  sumsnf  15094  tanval  15476  rpnnen2lem11  15572  rpnnen  15575  sadadd2lem  15801  sadadd3  15803  sadaddlem  15808  sadasslem  15812  sadeq  15814  lcmgcdlem  15943  unbenlem  16237  prmreclem6  16250  vdwlem8  16317  vdwnnlem1  16324  0ram  16349  structcnvcnv  16492  prdsval  16723  prdsbas  16725  prdsplusg  16726  prdsmulr  16727  prdsvsca  16728  prdshom  16735  xpsfrn  16836  xpsff1o2  16837  catcoppccl  17363  catcfuccl  17364  catcxpccl  17452  tsrss  17828  gsumpropd2lem  17884  smndex2dnrinv  18075  mvdco  18568  efgmnvl  18835  efgval  18838  efgi0  18841  efgi1  18842  efgredeu  18873  0frgp  18900  abln0  18983  lt6abl  19011  gsumval3  19023  gsum2dlem2  19087  dprdres  19146  dmdprdsplit2lem  19163  ringn0  19352  isdrng2  19508  drngmcl  19511  drngid2  19514  cnfldplusf  20121  cnfldsub  20122  cnsubmlem  20142  cnsubglem  20143  cnmsubglem  20157  gzrngunitlem  20159  rge0srg  20165  zring0  20176  zzngim  20247  zrhpsgnmhm  20276  re0g  20304  pjfval  20398  pjpm  20400  psrplusg  20622  coe1sfi  20845  ply1plusgfvi  20874  marep01ma  21268  smadiadetlem1a  21271  smadiadetlem3lem2  21275  smadiadetlem3  21276  smadiadetlem4  21277  smadiadet  21278  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  23552  xrhmeo  23554  cnheiborlem  23562  cnlmod  23748  lmmbr2  23866  lmcau  23920  metsscmetcld  23922  cncms  23962  cnfldcusp  23964  ovolctb  24097  ovoliunnul  24114  ismbl  24133  volf  24136  voliunlem1  24157  ioorf  24180  ioorinv  24183  ioorcl  24184  dyaddisj  24203  dyadmax  24205  dyadmbl  24207  mbfid  24242  ismbfd  24246  mbfimaopnlem  24262  limcresi  24491  dvreslem  24515  dvres2lem  24516  dvcjbr  24555  dvferm1  24591  dvferm2  24593  dvlip2  24601  dv11cn  24607  deg1ldg  24696  deg1leb  24699  plycpn  24888  vieta1lem2  24910  elqaa  24921  aalioulem2  24932  aaliou3lem3  24943  aaliou3lem4  24945  pserulm  25020  psercnlem2  25022  psercnlem1  25023  psercn  25024  abelth  25039  reeff1o  25045  pilem1  25049  efhalfpi  25067  coseq0negpitopi  25099  pige3ALT  25115  tanregt0  25134  efif1olem3  25139  efif1olem4  25140  efifo  25142  eff1olem  25143  efsubm  25146  logrn  25153  ellogrn  25154  relogf1o  25161  argregt0  25204  argrege0  25205  dvrelog  25231  dvloglem  25242  logf1o2  25244  dvlog  25245  efopnlem1  25250  efopnlem2  25251  logtayl  25254  cxpcn3lem  25339  cxpcn3  25340  resqrtcn  25341  asinneg  25475  asinrebnd  25490  atan0  25497  atanbnd  25515  areambl  25547  sqrtlim  25561  amgmlem  25578  lgamucov  25626  basellem1  25669  basellem4  25672  sqff1o  25770  dchrplusg  25834  bposlem6  25876  bposlem8  25878  dchrvmasumlem2  26085  mulog2sum  26124  pntibndlem1  26176  pntlemo  26194  qrng0  26208  ostth  26226  lmif  26582  islmib  26584  structiedg0val  26818  snstriedgval  26834  umgredgnlp  26943  usgrexmplef  27052  usgrexmpledg  27055  vtxdlfgrval  27278  upgr2pthnlp  27524  konigsberglem5  28044  ex-mod  28237  pliguhgr  28272  grporn  28307  ip0i  28611  ubthlem1  28656  ubthlem2  28657  axhcompl-zf  28784  normlem7  28902  bcseqi  28906  bcsiALT  28965  hlimf  29023  hlimuni  29024  hhssabloilem  29047  hhshsslem1  29053  hhsssh  29055  hhsscms  29064  occllem  29089  occl  29090  h1deoi  29335  h1dei  29336  h1de2ctlem  29341  h1de2ci  29342  spansni  29343  spanunsni  29365  pjpythi  29508  nmfn0  29773  nmopadjlem  29875  adjcoi  29886  nmopcoadji  29887  pjoccoi  29964  shatomistici  30147  iuninc  30327  imadifxp  30367  xppreima  30411  1stpreima  30469  2ndpreima  30470  fsuppcurry1  30490  fsuppcurry2  30491  hashgt1  30559  s3clhash  30653  gsummpt2d  30737  xrge0tsmsd  30745  tocyc01  30813  cyc3evpm  30845  cycpmconjslem2  30850  cyc3conja  30852  reofld  30967  rearchi  30969  nn0archi  30970  xrge0slmod  30971  elrspunidl  31017  dimval  31089  dimvalfi  31090  qtophaus  31189  iistmd  31253  xpinpreima  31257  xpinpreima2  31258  tpr2rico  31263  mndpluscn  31277  xrge0pluscn  31291  cnzh  31319  rezh  31320  qqhucn  31341  rrhcn  31346  cnrrext  31359  zrhre  31368  qqhre  31369  ismntop  31375  sigaex  31477  brsiga  31550  cntnevol  31595  voliune  31596  ddemeas  31603  1stmbfm  31626  2ndmbfm  31627  br2base  31635  dya2icoseg2  31644  dya2iocucvr  31650  carsgclctunlem2  31685  carsgclctunlem3  31686  sitgaddlemb  31714  eulerpartlemt  31737  eulerpartgbij  31738  eulerpartlemmf  31741  eulerpartlemgvv  31742  eulerpartlemgf  31745  eulerpart  31748  sseqmw  31757  sseqf  31758  sseqp1  31761  fiblem  31764  fibp1  31767  dstrvprob  31837  coinflipspace  31846  coinfliprv  31848  coinflippv  31849  ballotlem1  31852  ballotlem8  31902  circlemethhgt  32022  usgrcyclgt2v  32486  iccllysconn  32605  rellysconn  32606  satf00  32729  fmla0  32737  msrid  32900  dfrdg2  33148  trpredlem1  33174  trpredtr  33177  trpredmintr  33178  noextendseq  33282  dfrdg4  33520  imagesset  33522  elhf  33743  filnetlem3  33836  limsucncmpi  33901  bj-babygodel  34045  bj-idres  34570  taupilem3  34728  icoreresf  34764  icoreelrnab  34766  relowlssretop  34775  poimirlem3  35053  poimirlem9  35059  poimirlem15  35065  poimirlem16  35066  poimirlem17  35067  poimirlem19  35069  poimirlem27  35077  poimirlem28  35078  poimirlem31  35081  poimirlem32  35082  mblfinlem1  35087  ovoliunnfl  35092  voliunnfl  35094  mbfresfi  35096  dvtan  35100  itg2addnc  35104  ftc1anclem3  35125  areacirc  35143  fdc  35176  ismrer1  35269  reheibor  35270  rngomndo  35366  gidsn  35383  ac6s6f  35604  eccnvepex  35745  dfcnvrefrels2  35919  dfcnvrefrels3  35920  dedths  36251  tendo0co2  38077  erng1r  38284  dvalveclem  38314  dva0g  38316  dvh0g  38400  sn-dtru  39390  sn-it0e0  39539  sn-0tie0  39563  2rexfrabdioph  39724  3rexfrabdioph  39725  4rexfrabdioph  39726  6rexfrabdioph  39727  7rexfrabdioph  39728  rencldnfi  39749  jm2.27dlem2  39938  wepwso  39974  dfac11  39993  pwssplit4  40020  frlmpwfi  40029  isnumbasgrplem3  40036  mpaaeu  40081  proot1mul  40130  proot1hash  40131  cnvcnvintabd  40287  cnvrcl0  40312  dfrtrcl5  40316  cotrcltrcl  40413  frege92  40643  seff  41000  prmunb2  41002  binomcxplemdvbinom  41044  binomcxplemcvg  41045  binomcxplemnotnn0  41047  sumsnd  41642  islptre  42248  stoweidlem34  42663  stoweidlem37  42666  stirlinglem11  42713  stirlinglem12  42714  stirlinglem13  42715  fouriersw  42860  fundcmpsurbijinjpreimafv  43911  fundcmpsurinjimaid  43915  fmtnoinf  44040  gbowge7  44268  nnsum3primes4  44293  2zrng0  44549  lmodn0  44891  zlmodzxzldeplem3  44898  lvecpsslmod  44903  0dig2pr01  45011  aacllem  45316  amgmwlem  45317
  Copyright terms: Public domain W3C validator