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  2870  elnn  4638  intasym  5046  relcoi1  5188  funres11  5258  cnvresid  5260  fvex  5472  fparlem1  6152  fparlem2  6153  dftpos4  6187  tposf12  6193  tfr2b  6380  tz7.44lem1  6386  xpcomco  6920  sbthlem2  6940  fidomdm  7106  marypha1lem  7154  hartogslem1  7225  brwdom2  7255  inf3lem6  7302  omex  7312  cantnfdm  7333  cantnfval  7337  cantnff  7343  cnfcom  7371  cnfcom2  7373  cnfcom3lem  7374  cnfcom3  7375  tz9.1c  7380  r1tr  7416  r1ord3g  7419  rankwflemb  7433  r1elwf  7436  r1elss  7446  rankval3b  7466  onssr1  7471  infxpenlem  7609  alephnbtwn  7666  alephordilem1  7668  alephfp  7703  dfac13  7736  pwsdompw  7798  infcdaabs  7800  ackbij1  7832  ackbij2  7837  r1om  7838  cflim2  7857  fin23lem27  7922  fin23lem29  7935  fin23lem30  7936  fin1a2lem6  7999  fin1a2lem7  8000  fin1a2lem13  8006  itunitc1  8014  itunitc  8015  ituniiun  8016  hsmexlem5  8024  axcc2lem  8030  axcc3  8032  zorn2lem6  8096  zorn2lem7  8097  ttukeylem6  8109  axdc  8116  fodom  8117  iunfo  8129  cardval  8136  cardid  8137  pwcfsdom  8173  alephom  8175  fpwwe  8236  canthp1lem2  8243  canthp1  8244  gchaleph2  8266  r1limwun  8326  inaprc  8426  nqerf  8522  recmulnq  8556  dmrecnq  8560  halfnq  8568  genpdm  8594  reclem3pr  8641  axresscn  8738  axpre-sup  8759  1re  8805  0re  8806  00id  8955  addid1  8960  renegcli  9076  zexALT  10010  uzn0  10211  dfle2  10449  xrinfmss  10595  axdc4uzlem  11011  facnn  11257  fac0  11258  hashgval  11307  hashinf  11309  hashp1i  11335  hashxplem  11351  cats1fv  11475  cnrecnv  11616  rexanuz  11795  climdm  11994  lo1eq  12008  rlimeq  12009  sumsn  12179  tanval  12371  rpnnen2lem11  12466  rpnnen  12468  sadadd2lem  12613  sadadd3  12615  sadaddlem  12620  sadasslem  12624  sadeq  12626  3prm  12738  unbenlem  12918  prmreclem6  12931  vdwlem8  12998  vdwnnlem1  13005  0ram  13030  structcnvcnv  13122  prdsval  13318  prdsbas  13320  prdsplusg  13321  prdsmulr  13322  prdsvsca  13323  prdshom  13329  xpsfrn  13434  xpsff1o2  13436  catcoppccl  13903  catcfuccl  13904  catcxpccl  13944  tsrss  14295  symgid  14744  efgmnvl  14986  efgval  14989  efgi0  14992  efgi1  14993  efgredeu  15024  0frgp  15051  lt6abl  15144  gsumval3  15154  gsumzres  15157  gsumzadd  15167  gsum2d  15186  dprdfadd  15218  dprdres  15226  dmdprdsplit2lem  15243  isdrng2  15485  drngmcl  15488  drngid2  15491  psrplusg  16089  coe1sfi  16256  ply1plusgfvi  16283  cnfldplusf  16364  cnfldsub  16365  cnsubmlem  16382  cnmsubglem  16397  gzrngunitlem  16399  mulgghm2  16422  zzngim  16469  pjfval  16569  pjpm  16571  indistpsALT  16713  tgrest  16853  leordtval2  16905  lmbr2  16952  cnprest  16980  lmff  16992  kgenidm  17205  tx1cn  17266  tx2cn  17267  hausdiag  17302  tsmsres  17789  xmetge0  17872  qdensere  18242  cnblcld  18247  cnfldms  18248  cnfldtopn  18254  xrsdsre  18279  xrge0tsms  18302  iccpnfcnv  18405  xrhmeo  18407  cnheiborlem  18415  lmmbr2  18648  lmcau  18701  cmetss  18703  cncms  18737  ovolctb  18812  ovoliunnul  18829  ismbl  18848  volf  18851  voliunlem1  18870  ioorf  18891  ioorinv  18894  ioorcl  18895  dyaddisj  18914  dyadmax  18916  dyadmbl  18918  mbfid  18954  ismbfd  18958  mbfimaopnlem  18973  limcresi  19198  dvreslem  19222  dvres2lem  19223  dvcjbr  19261  dvferm1  19295  dvferm2  19297  dvlip2  19305  dv11cn  19311  tdeglem4  19409  deg1ldg  19441  deg1leb  19444  plycpn  19632  vieta1lem2  19654  elqaa  19665  aalioulem2  19676  aaliou3lem3  19687  aaliou3lem4  19689  pserulm  19761  psercnlem2  19763  psercnlem1  19764  psercn  19765  abelth  19780  reeff1o  19786  pilem1  19790  efhalfpi  19802  coseq0negpitopi  19834  pige3  19848  efif1olem3  19869  efif1olem4  19870  efifo  19872  eff1olem  19873  logrn  19879  ellogrn  19880  relogf1o  19887  argregt0  19927  argrege0  19928  dvrelog  19947  dvloglem  19958  logf1o2  19960  dvlog  19961  efopnlem1  19966  efopnlem2  19967  logtayl  19970  cxpcn3lem  20050  cxpcn3  20051  resqrcn  20052  asinneg  20145  asinrebnd  20160  atan0  20167  atanbnd  20185  areambl  20216  sqrlim  20230  amgmlem  20247  basellem1  20281  basellem4  20284  sqff1o  20383  dchrplusg  20449  bposlem6  20491  bposlem8  20493  lgseisenlem4  20554  dchrvmasumlem2  20610  dchrisum0flblem1  20620  mulog2sum  20649  pntibndlem1  20701  pntlemo  20719  qrng0  20733  ostth  20751  grporn  20840  issubgoi  20938  gidsn  20976  ginvsn  20977  rngomndo  21049  ip0i  21364  ubthlem1  21410  ubthlem2  21411  axhcompl-zf  21539  normlem7  21656  bcseqi  21660  bcsiALT  21719  hlimf  21778  hlimuni  21779  hhshsslem1  21805  hhsssh  21807  hhsscms  21817  occllem  21843  occl  21844  h1deoi  22089  h1dei  22090  h1de2ctlem  22095  h1de2ci  22096  spansni  22097  spanunsni  22119  pjpythi  22262  nmopadjlem  22630  adjcoi  22641  nmopcoadji  22642  pjoccoi  22719  shatomistici  22902  ballotlem1  23007  iccllyscon  23154  rellyscon  23155  vdegp1ai  23281  dfrdg2  23522  omsinds  23589  trpredlem1  23600  trpredtr  23603  trpredmintr  23604  wfrlem14  23639  dfrdg4  23864  elhf  24180  limsucncmpi  24260  scprefat  24438  scprefat2  24439  repfuntw  24528  domrancur1c  24570  bsi  24869  limptlimpr2lem2  24943  dtt1  24956  intrn  24967  bsi2  25007  bsi3  25009  bsi4  25011  addcanri  25034  issrc  25235  tartarmap  25256  prismorcsetlemc  25285  idcatfun  25309  lemindclsbu  25363  pgapspf  25420  pdiveql  25536  filnetlem3  25697  fdc  25823  ismrer1  25930  reheibor  25931  2rexfrabdioph  26245  3rexfrabdioph  26246  4rexfrabdioph  26247  6rexfrabdioph  26248  7rexfrabdioph  26249  rencldnfi  26272  jm2.27dlem2  26471  wepwso  26507  dfac11  26528  pwssplit4  26559  frlmpwfi  26630  isnumbasgrplem3  26638  mpaaeu  26723  mvdco  26756  proot1mul  26883  proot1hash  26887  seff  26906  sumsnd  27066  stoweidlem34  27152  stoweidlem37  27155  tendo0co2  30227  erng1r  30434  dvalveclem  30465  dva0g  30467  dvh0g  30551
This theorem was proved from axioms:  ax-mp 10
  Copyright terms: Public domain W3C validator