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  2060  2eu4  2239  inidm  3391  opcom  4276  opeqsn  4278  poirr  4341  asymref2  5076  xp11  5127  fununi  5332  brprcneu  5534  erinxp  6749  dom2lem  6917  pssnn  7097  dmaddpi  8530  dmmulpi  8531  gcddvds  12710  iscatd2  13599  isnsg2  14663  eqger  14683  gaorber  14778  efgcpbllemb  15080  xmeter  17995  caucfil  18725  subfaclefac  23722  axcontlem5  24667  apnei  25622  inixp  26501  2reu4a  28069  cusgra2v  28296  cusgra3v  28298  frgra3v  28425  eelT11  28787  uunT11  28884  uunT11p1  28885  uunT11p2  28886  uun111  28893  bnj594  29259  sbnf2NEW7  29579  equvelv  29738  cdlemg33b  31518
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