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

Theorem anidms 643
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
anidms.1  |-  ( (
ph  /\  ph )  ->  ps )
Assertion
Ref Expression
anidms  |-  ( ph  ->  ps )

Proof of Theorem anidms
StepHypRef Expression
1 anidms.1 . . 3  |-  ( (
ph  /\  ph )  ->  ps )
21ex 432 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 47 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  sylancb  663  sylancbr  664  dedth2v  3984  dedth3v  3985  dedth4v  3986  intsng  4307  pwnss  4602  snex  4678  isso2i  4821  posn  5057  xpid11  5213  f1oprswap  5837  f1o2sn  6050  residpr  6051  f1mpt  6144  f1eqcocnv  6179  isopolem  6216  3xpexg  6576  sqxpexg  6578  poxp  6885  oe0  7164  oecl  7179  nnmsucr  7266  ecopover  7407  enrefg  7540  php  7694  3xpfi  7784  dffi3  7883  infxpenlem  8382  xp2cda  8551  isfin5-2  8762  fpwwe2lem5  9001  pwfseqlem4a  9028  pwfseqlem4  9029  pwfseqlem5  9030  pwfseq  9031  nqereu  9296  halfnq  9343  ltsopr  9399  1idsr  9464  00sr  9465  sqgt0sr  9472  leid  9669  msqgt0  10069  msqge0  10070  recextlem1  10175  recextlem2  10176  recex  10177  div1  10232  cju  10527  2halves  10763  msqznn  10940  uzindOLD  10953  xrltnr  11333  xrleid  11359  iccid  11577  expubnd  12208  sqneg  12210  sqcl  12212  nnsqcl  12219  qsqcl  12221  subsq2  12258  bernneq  12274  faclbnd  12350  faclbnd3  12352  hashfac  12491  leiso  12492  cjmulval  13060  sin2t  13994  cos2t  13995  divalglem0  14135  divalglem2  14137  gcd0id  14245  isprm5  14337  prslem  15759  pslem  16035  dirref  16064  sgrp2nmndlem4  16245  grpsubid  16321  cntzi  16566  symgval  16603  symgbas  16604  symgbasfi  16610  symg1bas  16620  pgrpsubgsymg  16632  symgextfve  16643  pmtrfinv  16685  psgnsn  16744  lsmidm  16881  ipeq0  18846  matsca2  19089  matbas2  19090  matplusgcell  19102  matsubgcell  19103  mamulid  19110  mamurid  19111  mattposcl  19122  mat1dimelbas  19140  mat1dimscm  19144  m1detdiag  19266  mdetdiagid  19269  mdetunilem9  19289  pmatcoe1fsupp  19369  d1mat2pmat  19407  idcn  19925  hausdiag  20312  symgtgp  20766  ustref  20887  ustelimasn  20891  iducn  20952  ismet  20992  isxmet  20993  idnghm  21416  resubmet  21473  xrsxmet  21480  cphnm  21806  tchnmval  21838  ipcau2  21843  tchcphlem1  21844  tchcphlem2  21845  tchcph  21846  chordthmlem  23360  ismot  24123  is2wlkonot  25065  is2spthonot  25066  resgrprn  25480  ismgmOLD  25520  opidon2OLD  25524  rngo2  25588  vcoprnelem  25669  hmoval  25923  htth  26033  hvsubid  26141  hvnegid  26142  hv2times  26176  hiidrcl  26210  normval  26239  issh2  26324  chjidm  26636  normcan  26692  ho2times  26936  kbpj  27073  lnop0  27083  riesz3i  27179  leoprf  27245  leopsq  27246  cvnref  27408  gtiso  27747  prsss  28133  deranglem  28874  m1expevenALT  28927  fallrisefac  29388  dfpo2  29425  predpoirr  29517  predfrirr  29518  elfix2  29782  linedegen  30021  ftc1anclem3  30332  filnetlem2  30437  prdsbnd2  30531  reheibor  30575  exidreslem  30579  mzpf  30908  acongrep  31157  ttac  31217  mendval  31373  mendplusgfval  31375  mendmulrfval  31377  iocinico  31420  iocmbl  31421  seff  31430  sblpnf  31431  lcmid  31456  lcmgcdeq  31457  sigarid  32314  cnambpcma  32689  2leaddle2  32694  clintopval  32900  bj-ru0  34901
  Copyright terms: Public domain W3C validator