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

Theorem anidm 627
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 626 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 195 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  anidmdbi  629  anandi  803  anandir  804  nannot  1303  truantru  1346  falanfal  1349  nic-axALT  1449  sbnf2  2185  2eu4  2365  inidm  3551  opcom  4451  opeqsn  4453  poirr  4515  asymref2  5252  xp11  5305  fununi  5518  brprcneu  5722  erinxp  6979  dom2lem  7148  pssnn  7328  dmaddpi  8768  dmmulpi  8769  gcddvds  13016  iscatd2  13907  isnsg2  14971  eqger  14991  gaorber  15086  efgcpbllemb  15388  xmeter  18464  caucfil  19237  cusgra2v  21472  cusgra3v  21474  subfaclefac  24863  axcontlem5  25908  inixp  26431  2reu4a  27944  f13dfv  28082  frgra3v  28393  eelT11  28812  uunT11  28909  uunT11p1  28910  uunT11p2  28911  uun111  28918  bnj594  29284  sbnf2NEW7  29609  cdlemg33b  31505
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 179  df-an 362
  Copyright terms: Public domain W3C validator