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  1601  ceqsexv2d  3274  dtru  4887  intasym  5546  relcoi2  5701  funres11  6004  cnvresid  6006  idssxp  6047  elnn  7117  omsinds  7126  fparlem1  7322  fparlem2  7323  dftpos4  7416  tposf12  7422  wfrlem14  7473  tfr2b  7537  tz7.44lem1  7546  xpcomco  8091  sbthlem2  8112  fidomdm  8284  hartogslem1  8488  brwdom2  8519  inf3lem6  8568  omex  8578  cnfcom  8635  tz9.1c  8644  r1tr  8677  r1ord3g  8680  rankwflemb  8694  r1elwf  8697  r1elss  8707  rankval3b  8727  onssr1  8732  infxpenlem  8874  alephnbtwn  8932  alephordilem1  8934  alephfp  8969  dfac13  9002  pwsdompw  9064  infcdaabs  9066  ackbij1  9098  ackbij2  9103  r1om  9104  cflim2  9123  fin23lem27  9188  fin23lem29  9201  fin23lem30  9202  fin1a2lem6  9265  fin1a2lem7  9266  fin1a2lem13  9272  itunitc1  9280  itunitc  9281  ituniiun  9282  hsmexlem5  9290  axcc2lem  9296  axcc3  9298  zorn2lem6  9361  zorn2lem7  9362  ttukeylem6  9374  axdc  9381  fodom  9382  dmct  9384  iunfo  9399  cardval  9406  cardid  9407  pwcfsdom  9443  alephom  9445  canthp1lem2  9513  canthp1  9514  gchaleph2  9532  r1limwun  9596  inaprc  9696  nqerf  9790  recmulnq  9824  dmrecnq  9828  halfnq  9836  genpdm  9862  reclem3pr  9909  axresscn  10007  axpre-sup  10028  1re  10077  0re  10078  00id  10249  addid1  10254  renegcli  10380  zexALT  11434  uzn0  11741  dfle2  12018  xrinfmss  12178  xrge0neqmnf  12314  axdc4uzlem  12822  facnn  13102  fac0  13103  hashgval  13160  hashinf  13162  hashresfn  13168  hashrabrsn  13199  hashrabsn01  13200  hashrabsn1  13201  hashp1i  13229  hashxplem  13258  fi1uzind  13317  cshw1  13614  cats1fv  13650  trclubgi  13782  cnrecnv  13949  rexanuz  14129  climdm  14329  lo1eq  14343  rlimeq  14344  sumsnf  14517  sumsn  14519  tanval  14902  rpnnen2lem11  14997  rpnnen  15000  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  sadasslem  15239  sadeq  15241  lcmgcdlem  15366  3prm  15453  unbenlem  15659  prmreclem6  15672  vdwlem8  15739  vdwnnlem1  15746  0ram  15771  structcnvcnv  15918  prdsval  16162  prdsbas  16164  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdshom  16174  xpsfrn  16276  xpsff1o2  16278  catcoppccl  16805  catcfuccl  16806  catcxpccl  16894  tsrss  17270  gsumpropd2lem  17320  symgid  17867  mvdco  17911  efgmnvl  18173  efgval  18176  efgi0  18179  efgi1  18180  efgredeu  18211  0frgp  18238  abln0  18316  lt6abl  18342  gsumval3  18354  gsum2dlem2  18416  dprdres  18473  dmdprdsplit2lem  18490  ringn0  18649  isdrng2  18805  drngmcl  18808  drngid2  18811  psrplusg  19429  coe1sfi  19631  ply1plusgfvi  19660  cnfldplusf  19821  cnfldsub  19822  cnsubmlem  19842  cnmsubglem  19857  gzrngunitlem  19859  rge0srg  19865  zring0  19876  zzngim  19949  zrhpsgnmhm  19978  re0g  20006  pjfval  20098  pjpm  20100  marep01ma  20514  smadiadetlem1a  20517  smadiadetlem3lem2  20521  smadiadetlem3  20522  smadiadetlem4  20523  smadiadet  20524  indistpsALT  20865  tgrest  21011  leordtval2  21064  lmbr2  21111  cnprest  21141  lmff  21153  kgenidm  21398  tx1cn  21460  tx2cn  21461  hausdiag  21496  elrnust  22075  ustbas  22078  psmetge0  22164  xmetge0  22196  qdensere  22620  cnblcld  22625  cnfldms  22626  cnfldtopn  22632  xrsdsre  22660  xrge0tsms  22684  iccpnfcnv  22790  xrhmeo  22792  cnheiborlem  22800  cnlmod  22986  lmmbr2  23103  lmcau  23157  cmetss  23159  cncms  23197  cnfldcusp  23199  ovolctb  23304  ovoliunnul  23321  ismbl  23340  volf  23343  voliunlem1  23364  ioorf  23387  ioorinv  23390  ioorcl  23391  dyaddisj  23410  dyadmax  23412  dyadmbl  23414  mbfid  23448  ismbfd  23452  mbfimaopnlem  23467  limcresi  23694  dvreslem  23718  dvres2lem  23719  dvcjbr  23757  dvferm1  23793  dvferm2  23795  dvlip2  23803  dv11cn  23809  deg1ldg  23897  deg1leb  23900  plycpn  24089  vieta1lem2  24111  elqaa  24122  aalioulem2  24133  aaliou3lem3  24144  aaliou3lem4  24146  pserulm  24221  psercnlem2  24223  psercnlem1  24224  psercn  24225  abelth  24240  reeff1o  24246  pilem1  24250  efhalfpi  24268  coseq0negpitopi  24300  pige3  24314  tanregt0  24330  efif1olem3  24335  efif1olem4  24336  efifo  24338  eff1olem  24339  efsubm  24342  logrn  24350  ellogrn  24351  relogf1o  24358  argregt0  24401  argrege0  24402  dvrelog  24428  dvloglem  24439  logf1o2  24441  dvlog  24442  efopnlem1  24447  efopnlem2  24448  logtayl  24451  cxpcn3lem  24533  cxpcn3  24534  resqrtcn  24535  asinneg  24658  asinrebnd  24673  atan0  24680  atanbnd  24698  areambl  24730  sqrtlim  24744  amgmlem  24761  lgamucov  24809  basellem1  24852  basellem4  24855  sqff1o  24953  dchrplusg  25017  bposlem6  25059  bposlem8  25061  dchrvmasumlem2  25232  mulog2sum  25271  pntibndlem1  25323  pntlemo  25341  qrng0  25355  ostth  25373  lmif  25722  islmib  25724  structiedg0val  25956  snstriedgval  25975  vtxvalsnop  25978  iedgvalsnop  25979  umgredgnlp  26087  usgrexmplef  26196  usgrexmpledg  26199  vtxdlfgrval  26437  upgr2pthnlp  26684  konigsberglem5  27234  ex-mod  27436  pliguhgr  27468  grporn  27503  ip0i  27808  ubthlem1  27854  ubthlem2  27855  axhcompl-zf  27983  normlem7  28101  bcseqi  28105  bcsiALT  28164  hlimf  28222  hlimuni  28223  hhssabloilem  28246  hhshsslem1  28252  hhsssh  28254  hhsscms  28264  occllem  28290  occl  28291  h1deoi  28536  h1dei  28537  h1de2ctlem  28542  h1de2ci  28543  spansni  28544  spanunsni  28566  pjpythi  28709  nmfn0  28974  nmopadjlem  29076  adjcoi  29087  nmopcoadji  29088  pjoccoi  29165  shatomistici  29348  imadifxp  29540  xppreima  29577  1stpreima  29612  2ndpreima  29613  gsummpt2d  29909  xrge0tsmsd  29913  reofld  29968  rearchi  29970  nn0archi  29971  xrge0slmod  29972  qtophaus  30031  iistmd  30076  xpinpreima  30080  xpinpreima2  30081  tpr2rico  30086  mndpluscn  30100  xrge0pluscn  30114  cnzh  30142  rezh  30143  qqhucn  30164  rrhcn  30169  cnrrext  30182  zrhre  30191  qqhre  30192  ismntop  30198  sigaex  30300  brsiga  30374  cntnevol  30419  voliune  30420  ddemeas  30427  1stmbfm  30450  2ndmbfm  30451  br2base  30459  dya2icoseg2  30468  dya2iocucvr  30474  carsgclctunlem2  30509  carsgclctunlem3  30510  sitgaddlemb  30538  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemmf  30565  eulerpartlemgvv  30566  eulerpartlemgf  30569  eulerpart  30572  sseqmw  30581  sseqf  30582  sseqp1  30585  fiblem  30588  fibp1  30591  dstrvprob  30661  coinflipspace  30670  coinfliprv  30672  coinflippv  30673  ballotlem1  30676  ballotlem8  30726  circlemethhgt  30849  iccllysconn  31358  rellysconn  31359  msrid  31568  dfrdg2  31825  trpredlem1  31851  trpredtr  31854  trpredmintr  31855  noextendseq  31945  dfrdg4  32183  imagesset  32185  elhf  32406  filnetlem3  32500  limsucncmpi  32569  taupilem3  33295  icoreresf  33330  icoreelrnab  33332  relowlssretop  33341  poimirlem3  33542  poimirlem9  33548  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  mblfinlem1  33576  ovoliunnfl  33581  voliunnfl  33583  mbfresfi  33586  dvtan  33590  itg2addnc  33594  ftc1anclem3  33617  areacirc  33635  fdc  33671  ismrer1  33767  reheibor  33768  rngomndo  33864  gidsn  33881  ac6s6f  34111  dfcnvrefrels2  34416  dfcnvrefrels3  34417  dedths  34566  tendo0co2  36393  erng1r  36600  dvalveclem  36631  dva0g  36633  dvh0g  36717  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  rencldnfi  37702  jm2.27dlem2  37894  wepwso  37930  dfac11  37949  pwssplit4  37976  frlmpwfi  37985  isnumbasgrplem3  37992  mpaaeu  38037  proot1mul  38094  proot1hash  38095  cnvcnvintabd  38223  rtrclex  38241  cnvrcl0  38249  dfrtrcl5  38253  frege92  38566  seff  38825  prmunb2  38827  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemnotnn0  38872  sumsnd  39499  islptre  40169  stoweidlem34  40569  stoweidlem37  40572  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  fouriersw  40766  fmtnoinf  41773  gbowge7  41976  nnsum3primes4  42001  2zrng0  42263  lmodn0  42609  zlmodzxzldeplem3  42616  lvecpsslmod  42621  0dig2pr01  42729  aacllem  42875  amgmwlem  42876
  Copyright terms: Public domain W3C validator