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

Theorem anidm 625
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 624 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 193 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  anidmdbi  627  anandi  801  anandir  802  nannot  1293  truantru  1326  falanfal  1329  nic-axALT  1429  sbnf2  2047  2eu4  2226  inidm  3378  opcom  4260  opeqsn  4262  poirr  4325  asymref2  5060  xp11  5111  fununi  5316  brprcneu  5518  erinxp  6733  dom2lem  6901  pssnn  7081  dmaddpi  8514  dmmulpi  8515  gcddvds  12694  iscatd2  13583  isnsg2  14647  eqger  14667  gaorber  14762  efgcpbllemb  15064  xmeter  17979  caucfil  18709  subfaclefac  23707  axcontlem5  24596  apnei  25520  inixp  26399  2reu4a  27967  cusgra2v  28158  frgra3v  28180  eelT11  28483  uunT11  28571  uunT11p1  28572  uunT11p2  28573  uun111  28580  bnj594  28944  equvelv  29116  cdlemg33b  30896
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 177  df-an 360
  Copyright terms: Public domain W3C validator