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

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

Proof of Theorem anidm
StepHypRef Expression
1 pm4.24 643 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 202 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  anidmdbi  646  anandi  824  anandir  825  nannot  1340  truantru  1394  falanfal  1397  nic-axALT  1482  sbnf2OLD  2154  2eu4OLD  2378  inidm  3666  opcom  4692  opeqsn  4694  poirr  4759  asymref2  5322  xp11  5380  fununi  5591  brprcneu  5791  erinxp  7283  dom2lem  7458  pssnn  7641  dmaddpi  9169  dmmulpi  9170  gcddvds  13816  iscatd2  14737  isnsg2  15829  eqger  15849  gaorber  15944  efgcpbllemb  16372  xmeter  20139  caucfil  20925  axcontlem5  23365  cusgra2v  23521  cusgra3v  23523  disjunsn  26086  subfaclefac  27207  inixp  28769  2reu4a  30160  f13dfv  30294  erclwwlkref  30630  erclwwlknref  30646  frgra3v  30741  eelT11  31749  uunT11  31846  uunT11p1  31847  uunT11p2  31848  uun111  31855  bnj594  32222  cdlemg33b  34674
  Copyright terms: Public domain W3C validator