MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2b Unicode version

Theorem mp2b 11
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
Hypotheses
Ref Expression
mp2b.1  |-  ph
mp2b.2  |-  ( ph  ->  ps )
mp2b.3  |-  ( ps 
->  ch )
Assertion
Ref Expression
mp2b  |-  ch

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3  |-  ph
2 mp2b.2 . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 10 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 10 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  eqvinc  2832  elnn  4557  intasym  4965  relcoi1  5107  funres11  5177  cnvresid  5179  fvex  5391  fparlem1  6070  fparlem2  6071  dftpos4  6105  tposf12  6111  tfr2b  6298  tz7.44lem1  6304  xpcomco  6837  sbthlem2  6857  fidomdm  7023  marypha1lem  7070  hartogslem1  7141  brwdom2  7171  inf3lem6  7218  omex  7228  cantnfdm  7249  cantnfval  7253  cantnff  7259  cnfcom  7287  cnfcom2  7289  cnfcom3lem  7290  cnfcom3  7291  tz9.1c  7296  r1tr  7332  r1ord3g  7335  rankwflemb  7349  r1elwf  7352  r1elss  7362  rankval3b  7382  onssr1  7387  infxpenlem  7525  alephnbtwn  7582  alephordilem1  7584  alephfp  7619  dfac13  7652  pwsdompw  7714  infcdaabs  7716  ackbij1  7748  ackbij2  7753  r1om  7754  cflim2  7773  fin23lem27  7838  fin23lem29  7851  fin23lem30  7852  fin1a2lem6  7915  fin1a2lem7  7916  fin1a2lem13  7922  itunitc1  7930  itunitc  7931  ituniiun  7932  hsmexlem5  7940  axcc2lem  7946  axcc3  7948  zorn2lem6  8012  zorn2lem7  8013  ttukeylem6  8025  axdc  8032  fodom  8033  iunfo  8045  cardval  8052  cardid  8053  pwcfsdom  8085  alephom  8087  fpwwe  8148  canthp1lem2  8155  canthp1  8156  gchaleph2  8178  r1limwun  8238  inaprc  8338  nqerf  8434  recmulnq  8468  dmrecnq  8472  halfnq  8480  genpdm  8506  reclem3pr  8553  axresscn  8650  axpre-sup  8671  1re  8717  0re  8718  00id  8867  addid1  8872  renegcli  8988  zexALT  9921  uzn0  10122  dfle2  10360  xrinfmss  10506  axdc4uzlem  10922  facnn  11168  fac0  11169  hashgval  11218  hashinf  11220  hashp1i  11246  hashxplem  11262  cats1fv  11386  cnrecnv  11527  rexanuz  11706  climdm  11905  lo1eq  11919  rlimeq  11920  sumsn  12090  tanval  12282  rpnnen2lem11  12377  rpnnen  12379  sadadd2lem  12524  sadadd3  12526  sadaddlem  12531  sadasslem  12535  sadeq  12537  3prm  12649  unbenlem  12829  prmreclem6  12842  vdwlem8  12909  vdwnnlem1  12916  0ram  12941  structcnvcnv  13033  prdsval  13229  prdsbas  13231  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdshom  13240  xpsfrn  13345  xpsff1o2  13347  catcoppccl  13784  catcfuccl  13785  catcxpccl  13825  tsrss  14167  symgid  14616  efgmnvl  14858  efgval  14861  efgi0  14864  efgi1  14865  efgredeu  14896  0frgp  14923  lt6abl  15016  gsumval3  15026  gsumzres  15029  gsumzadd  15039  gsum2d  15058  dprdfadd  15090  dprdres  15098  dmdprdsplit2lem  15115  isdrng2  15357  drngmcl  15360  drngid2  15363  psrplusg  15958  coe1sfi  16125  ply1plusgfvi  16152  cnfldplusf  16233  cnfldsub  16234  cnsubmlem  16251  cnmsubglem  16266  gzrngunitlem  16268  mulgghm2  16291  zzngim  16338  pjfval  16438  pjpm  16440  indistpsALT  16582  tgrest  16722  leordtval2  16774  lmbr2  16821  cnprest  16849  lmff  16861  kgenidm  17074  tx1cn  17135  tx2cn  17136  hausdiag  17171  tsmsres  17658  xmetge0  17741  qdensere  18111  cnblcld  18116  cnfldms  18117  cnfldtopn  18123  xrsdsre  18148  xrge0tsms  18171  iccpnfcnv  18274  xrhmeo  18276  cnheiborlem  18284  lmmbr2  18517  lmcau  18570  cmetss  18572  cncms  18606  ovolctb  18681  ovoliunnul  18698  ismbl  18717  volf  18720  voliunlem1  18739  ioorf  18760  ioorinv  18763  ioorcl  18764  dyaddisj  18783  dyadmax  18785  dyadmbl  18787  mbfid  18823  ismbfd  18827  mbfimaopnlem  18842  limcresi  19067  dvreslem  19091  dvres2lem  19092  dvcjbr  19130  dvferm1  19164  dvferm2  19166  dvlip2  19174  dv11cn  19180  tdeglem4  19278  deg1ldg  19310  deg1leb  19313  plycpn  19501  vieta1lem2  19523  elqaa  19534  aalioulem2  19545  aaliou3lem3  19556  aaliou3lem4  19558  pserulm  19630  psercnlem2  19632  psercnlem1  19633  psercn  19634  abelth  19649  reeff1o  19655  pilem1  19659  efhalfpi  19671  coseq0negpitopi  19703  pige3  19717  efif1olem3  19738  efif1olem4  19739  efifo  19741  eff1olem  19742  logrn  19748  ellogrn  19749  relogf1o  19756  argregt0  19796  argrege0  19797  dvrelog  19816  dvloglem  19827  logf1o2  19829  dvlog  19830  efopnlem1  19835  efopnlem2  19836  logtayl  19839  cxpcn3lem  19955  cxpcn3  19956  resqrcn  19957  asinneg  20014  asinrebnd  20029  atan0  20036  atanbnd  20054  areambl  20085  sqrlim  20099  amgmlem  20116  basellem1  20150  basellem4  20153  sqff1o  20252  dchrplusg  20318  bposlem6  20360  bposlem8  20362  lgseisenlem4  20423  dchrvmasumlem2  20479  dchrisum0flblem1  20489  mulog2sum  20518  pntibndlem1  20570  pntlemo  20588  qrng0  20602  ostth  20620  grporn  20709  issubgoi  20807  gidsn  20845  ginvsn  20846  rngomndo  20918  ip0i  21233  ubthlem1  21279  ubthlem2  21280  axhcompl-zf  21408  normlem7  21525  bcseqi  21529  bcsiALT  21588  hlimf  21647  hlimuni  21648  hhshsslem1  21674  hhsssh  21676  hhsscms  21686  occllem  21712  occl  21713  h1deoi  21958  h1dei  21959  h1de2ctlem  21964  h1de2ci  21965  spansni  21966  spanunsni  21988  pjpythi  22149  nmopadjlem  22499  adjcoi  22510  nmopcoadji  22511  pjoccoi  22588  shatomistici  22771  iccllyscon  22952  rellyscon  22953  vdegp1ai  23079  dfrdg2  23320  omsinds  23387  trpredlem1  23398  trpredtr  23401  trpredmintr  23402  wfrlem14  23437  dfrdg4  23662  elhf  23978  limsucncmpi  24058  scprefat  24236  scprefat2  24237  repfuntw  24326  domrancur1c  24368  bsi  24667  limptlimpr2lem2  24741  dtt1  24754  intrn  24765  bsi2  24805  bsi3  24807  bsi4  24809  addcanri  24832  issrc  25033  tartarmap  25054  prismorcsetlemc  25083  idcatfun  25107  lemindclsbu  25161  pgapspf  25218  pdiveql  25334  filnetlem3  25495  fdc  25621  ismrer1  25728  reheibor  25729  2rexfrabdioph  26043  3rexfrabdioph  26044  4rexfrabdioph  26045  6rexfrabdioph  26046  7rexfrabdioph  26047  rencldnfi  26070  jm2.27dlem2  26269  wepwso  26305  dfac11  26326  pwssplit4  26357  frlmpwfi  26428  isnumbasgrplem3  26436  mpaaeu  26521  mvdco  26554  proot1mul  26681  proot1hash  26685  seff  26704  tendo0co2  29778  erng1r  29985  dvalveclem  30016  dva0g  30018  dvh0g  30102
This theorem was proved from axioms:  ax-mp 10
  Copyright terms: Public domain W3C validator