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

Theorem anidm 626
Description: Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)
Assertion
Ref Expression
anidm  |-  ( (
ph  /\  ph )  <->  ph )

Proof of Theorem anidm
StepHypRef Expression
1 pm4.24 625 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 194 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  anidmdbi  628  anandi  802  anandir  803  nannot  1299  truantru  1342  falanfal  1345  nic-axALT  1445  sbnf2  2134  2eu4  2314  inidm  3486  opcom  4384  opeqsn  4386  poirr  4448  asymref2  5184  xp11  5237  fununi  5450  brprcneu  5654  erinxp  6907  dom2lem  7076  pssnn  7256  dmaddpi  8693  dmmulpi  8694  gcddvds  12935  iscatd2  13826  isnsg2  14890  eqger  14910  gaorber  15005  efgcpbllemb  15307  xmeter  18346  caucfil  19100  cusgra2v  21330  cusgra3v  21332  subfaclefac  24634  axcontlem5  25614  inixp  26114  2reu4a  27628  frgra3v  27748  eelT11  28145  uunT11  28242  uunT11p1  28243  uunT11p2  28244  uun111  28251  bnj594  28614  sbnf2NEW7  28934  equvelv  29092  cdlemg33b  30872
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