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

Theorem anidms 627
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 424 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 45 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylancb  647  sylancbr  648  dedth2v  3776  dedth3v  3777  dedth4v  3778  intsng  4077  pwnss  4357  snex  4397  isso2i  4527  posn  4938  xpid11  5083  resiexg  5180  f1oprswap  5709  f1mpt  5999  f1eqcocnv  6020  isopolem  6057  poxp  6450  oe0  6758  oecl  6773  nnmsucr  6860  erex  6921  ecopover  7000  enrefg  7131  php  7283  dffi3  7428  hartogslem2  7504  harwdom  7550  infxpenlem  7887  dfac8b  7904  ac10ct  7907  xp2cda  8052  isfin5-2  8263  fpwwe2lem5  8501  canthwe  8518  pwfseqlem4a  8528  pwfseqlem4  8529  pwfseqlem5  8530  pwfseq  8531  nqereu  8798  halfnq  8845  ltsopr  8901  1idsr  8965  00sr  8966  sqgt0sr  8973  leid  9161  msqgt0  9540  msqge0  9541  recextlem1  9644  recextlem2  9645  recex  9646  div1  9699  cju  9988  2halves  10188  msqznn  10343  uzindOLD  10356  xrltnr  10712  xrleid  10735  iccid  10953  expubnd  11432  sqneg  11434  sqcl  11436  nnsqcl  11443  qsqcl  11445  subsq2  11481  bernneq  11497  faclbnd  11573  faclbnd3  11575  hashfac  11699  leiso  11700  cjmulval  11942  sin2t  12770  cos2t  12771  divalglem0  12905  divalglem2  12907  gcd0id  13015  isprm5  13104  ssclem  14011  prslem  14380  ipolerval  14574  pslem  14630  dirref  14672  grpsubid  14865  symgval  15086  symgbas  15087  cntzi  15120  lsmidm  15288  ipeq0  16861  idcn  17313  hausdiag  17669  symgtgp  18123  ustval  18224  isust  18225  ustref  18240  ustelimasn  18244  restutopopn  18260  ressuss  18285  iducn  18305  ispsmet  18327  ismet  18345  isxmet  18346  idnghm  18769  resubmet  18825  xrsxmet  18832  cphnm  19148  tchnmval  19179  ipcau2  19183  tchcphlem1  19184  tchcphlem2  19185  tchcph  19186  chordthmlem  20665  resgrprn  21860  ismgm  21900  opidon2  21904  rngo2  21968  vcoprnelem  22049  hmoval  22303  htth  22413  hvsubid  22520  hvnegid  22521  hv2times  22555  hiidrcl  22589  normval  22618  issh2  22703  chjidm  23014  normcan  23070  ho2times  23314  kbpj  23451  lnop0  23461  riesz3i  23557  leoprf  23623  leopsq  23624  cvnref  23786  gtiso  24080  deranglem  24844  m1expevenALT  24897  fallrisefac  25333  dfpo2  25370  predpoirr  25464  predfrirr  25465  elfix2  25741  linedegen  26069  ftc1anclem3  26272  filnetlem2  26399  prdsbnd2  26495  reheibor  26539  exidreslem  26543  mzpf  26784  acongrep  27036  ttac  27098  pmtrfinv  27370  mamulid  27426  mamurid  27427  matsca2  27442  matbas2  27443  matlmod  27447  mendval  27459  mendplusgfval  27461  mendmulrfval  27463  seff  27506  sblpnf  27507  sigarid  27815  3xpexg  28044  3xpfi  28072  2leaddle2  28077  is2wlkonot  28283  is2spthonot  28284  2wlkonot  28285  2spthonot  28286  2spotfi  28312  2spotmdisj  28394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator