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  2157  2eu4  2337  inidm  3510  opcom  4410  opeqsn  4412  poirr  4474  asymref2  5210  xp11  5263  fununi  5476  brprcneu  5680  erinxp  6937  dom2lem  7106  pssnn  7286  dmaddpi  8723  dmmulpi  8724  gcddvds  12970  iscatd2  13861  isnsg2  14925  eqger  14945  gaorber  15040  efgcpbllemb  15342  xmeter  18416  caucfil  19189  cusgra2v  21424  cusgra3v  21426  subfaclefac  24815  axcontlem5  25811  inixp  26320  2reu4a  27834  f13dfv  27962  nn0fz0  27979  frgra3v  28106  eelT11  28520  uunT11  28617  uunT11p1  28618  uunT11p2  28619  uun111  28626  bnj594  28989  sbnf2NEW7  29309  cdlemg33b  31189
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