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

Theorem anidms 651
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 436 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  sylancb  671  sylancbr  672  dedth2v  3936  dedth3v  3937  dedth4v  3938  intsng  4270  pwnss  4568  snex  4641  isso2i  4787  posn  4903  xpid11  5056  predpoirr  5408  predfrirr  5409  f1oprswap  5854  f1o2sn  6067  residpr  6068  f1mpt  6162  f1eqcocnv  6199  isopolem  6236  3xpexg  6594  sqxpexg  6596  poxp  6908  oe0  7224  oecl  7239  nnmsucr  7326  ecopover  7467  enrefg  7601  php  7756  3xpfi  7843  dffi3  7945  infxpenlem  8444  xp2cda  8610  isfin5-2  8821  fpwwe2lem5  9059  pwfseqlem4a  9086  pwfseqlem4  9087  pwfseqlem5  9088  pwfseq  9089  nqereu  9354  halfnq  9401  ltsopr  9457  1idsr  9522  00sr  9523  sqgt0sr  9530  leid  9729  msqgt0  10134  msqge0  10135  recextlem1  10242  recextlem2  10243  recex  10244  div1  10299  cju  10605  2halves  10841  msqznn  11017  xrltnr  11421  xrleid  11449  iccid  11681  m1expeven  12319  expubnd  12333  sqneg  12335  sqcl  12337  nnsqcl  12344  qsqcl  12346  subsq2  12383  bernneq  12398  faclbnd  12475  faclbnd3  12477  hashfac  12621  leiso  12622  cjmulval  13208  fallrisefac  14078  sin2t  14231  cos2t  14232  divalglem0  14371  divalglem2  14373  divalglem2OLD  14374  gcd0id  14487  lcmid  14574  lcmgcdeq  14577  lcmfsn  14608  isprm5  14651  prslem  16176  pslem  16452  dirref  16481  sgrp2nmndlem4  16662  grpsubid  16738  cntzi  16983  symgval  17020  symgbas  17021  symgbasfi  17027  symg1bas  17037  pgrpsubgsymg  17049  symgextfve  17060  pmtrfinv  17102  psgnsn  17161  lsmidm  17314  ipeq0  19205  matsca2  19445  matbas2  19446  matplusgcell  19458  matsubgcell  19459  mamulid  19466  mamurid  19467  mattposcl  19478  mat1dimelbas  19496  mat1dimscm  19500  m1detdiag  19622  mdetdiagid  19625  mdetunilem9  19645  pmatcoe1fsupp  19725  d1mat2pmat  19763  idcn  20273  hausdiag  20660  symgtgp  21116  ustref  21233  ustelimasn  21237  iducn  21298  ismet  21338  isxmet  21339  idnghm  21764  resubmet  21820  xrsxmet  21827  cphnm  22171  tchnmval  22203  ipcau2  22208  tchcphlem1  22209  tchcphlem2  22210  tchcph  22211  chordthmlem  23758  ismot  24580  is2wlkonot  25591  is2spthonot  25592  resgrprn  26008  ismgmOLD  26048  opidon2OLD  26052  rngo2  26116  vcoprnelem  26197  hmoval  26451  htth  26571  hvsubid  26679  hvnegid  26680  hv2times  26714  hiidrcl  26748  normval  26777  issh2  26862  chjidm  27173  normcan  27229  ho2times  27472  kbpj  27609  lnop0  27619  riesz3i  27715  leoprf  27781  leopsq  27782  cvnref  27944  gtiso  28281  prsss  28722  deranglem  29889  dfpo2  30395  elfix2  30671  linedegen  30910  filnetlem2  31035  bj-ru0  31537  ftc1anclem3  32019  prdsbnd2  32127  reheibor  32171  exidreslem  32175  mzpf  35578  acongrep  35830  ttac  35891  mendval  36049  mendplusgfval  36051  mendmulrfval  36053  iocinico  36096  iocmbl  36097  seff  36657  sblpnf  36658  sigarid  38467  opidg  38997  cnambpcma  39040  2leaddle2  39044  clintopval  39893
  Copyright terms: Public domain W3C validator