Theorem anidm 644

Description: Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Assertion

Ref	Expression
anidm

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm4.24 643	. 2
2	1	bicomi 202	1

Syntax hints:  <->wb 184  /\wa 369

This theorem is referenced by:  anidmdbi  646  anandi  828  anandir  829  nannot  1351  truantru  1419  falanfal  1422  nic-axALT  1507  2eu4OLD  2381  inidm  3706  opcom  4746  opeqsn  4748  poirr  4816  asymref2  5389  xp11  5447  fununi  5659  brprcneu  5864  f13dfv  6180  erinxp  7404  dom2lem  7575  pssnn  7758  dmaddpi  9289  dmmulpi  9290  gcddvds  14153  iscatd2  15078  isnsg2  16231  eqger  16251  gaorber  16346  efgcpbllemb  16773  xmeter  20936  caucfil  21722  axcontlem5  24271  cusgra2v  24462  cusgra3v  24464  erclwwlkref  24813  erclwwlknref  24825  frgra3v  25002  disjunsn  27453  subfaclefac  28620  inixp  30219  2reu4a  32194  dfiso2  32568  eelT11  33496  uunT11  33593  uunT11p1  33594  uunT11p2  33595  uun111  33602  bnj594  33970  cdlemg33b  36433

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 371