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

Theorem anidms 649
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 435 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
32pm2.43i 49 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  sylancb  669  sylancbr  670  dedth2v  3961  dedth3v  3962  dedth4v  3963  intsng  4285  pwnss  4581  snex  4654  isso2i  4798  posn  4914  xpid11  5067  predpoirr  5418  predfrirr  5419  f1oprswap  5861  f1o2sn  6073  residpr  6074  f1mpt  6168  f1eqcocnv  6205  isopolem  6242  3xpexg  6599  sqxpexg  6601  poxp  6910  oe0  7223  oecl  7238  nnmsucr  7325  ecopover  7466  enrefg  7599  php  7753  3xpfi  7840  dffi3  7942  infxpenlem  8434  xp2cda  8599  isfin5-2  8810  fpwwe2lem5  9048  pwfseqlem4a  9075  pwfseqlem4  9076  pwfseqlem5  9077  pwfseq  9078  nqereu  9343  halfnq  9390  ltsopr  9446  1idsr  9511  00sr  9512  sqgt0sr  9519  leid  9718  msqgt0  10123  msqge0  10124  recextlem1  10231  recextlem2  10232  recex  10233  div1  10288  cju  10594  2halves  10830  msqznn  11006  xrltnr  11410  xrleid  11438  iccid  11670  m1expeven  12305  expubnd  12319  sqneg  12321  sqcl  12323  nnsqcl  12330  qsqcl  12332  subsq2  12369  bernneq  12384  faclbnd  12461  faclbnd3  12463  hashfac  12605  leiso  12606  cjmulval  13176  fallrisefac  14045  sin2t  14198  cos2t  14199  divalglem0  14338  divalglem2  14340  gcd0id  14450  lcmid  14534  lcmgcdeq  14537  lcmfsn  14568  isprm5  14611  prslem  16120  pslem  16396  dirref  16425  sgrp2nmndlem4  16606  grpsubid  16682  cntzi  16927  symgval  16964  symgbas  16965  symgbasfi  16971  symg1bas  16981  pgrpsubgsymg  16993  symgextfve  17004  pmtrfinv  17046  psgnsn  17105  lsmidm  17242  ipeq0  19129  matsca2  19369  matbas2  19370  matplusgcell  19382  matsubgcell  19383  mamulid  19390  mamurid  19391  mattposcl  19402  mat1dimelbas  19420  mat1dimscm  19424  m1detdiag  19546  mdetdiagid  19549  mdetunilem9  19569  pmatcoe1fsupp  19649  d1mat2pmat  19687  idcn  20197  hausdiag  20584  symgtgp  21040  ustref  21157  ustelimasn  21161  iducn  21222  ismet  21262  isxmet  21263  idnghm  21668  resubmet  21724  xrsxmet  21731  cphnm  22057  tchnmval  22089  ipcau2  22094  tchcphlem1  22095  tchcphlem2  22096  tchcph  22097  chordthmlem  23620  ismot  24437  is2wlkonot  25433  is2spthonot  25434  resgrprn  25850  ismgmOLD  25890  opidon2OLD  25894  rngo2  25958  vcoprnelem  26039  hmoval  26293  htth  26403  hvsubid  26511  hvnegid  26512  hv2times  26546  hiidrcl  26580  normval  26609  issh2  26694  chjidm  27005  normcan  27061  ho2times  27304  kbpj  27441  lnop0  27451  riesz3i  27547  leoprf  27613  leopsq  27614  cvnref  27776  gtiso  28118  prsss  28558  deranglem  29674  dfpo2  30179  elfix2  30453  linedegen  30692  filnetlem2  30817  bj-ru0  31283  ftc1anclem3  31723  prdsbnd2  31831  reheibor  31875  exidreslem  31879  mzpf  35287  acongrep  35540  ttac  35601  mendval  35752  mendplusgfval  35754  mendmulrfval  35756  iocinico  35799  iocmbl  35800  seff  36298  sblpnf  36299  sigarid  37871  cnambpcma  38402  2leaddle2  38406  clintopval  38611
  Copyright terms: Public domain W3C validator