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  828  anandir  829  nannot  1352  truantru  1407  falanfal  1410  nic-axALT  1494  2eu4OLD  2367  inidm  3692  opcom  4731  opeqsn  4733  poirr  4801  asymref2  5374  xp11  5432  fununi  5644  brprcneu  5849  f13dfv  6165  erinxp  7387  dom2lem  7557  pssnn  7740  dmaddpi  9271  dmmulpi  9272  gcddvds  14135  iscatd2  15060  isnsg2  16210  eqger  16230  gaorber  16325  efgcpbllemb  16752  xmeter  20914  caucfil  21700  axcontlem5  24249  cusgra2v  24440  cusgra3v  24442  erclwwlkref  24791  erclwwlknref  24803  frgra3v  24980  disjunsn  27431  subfaclefac  28598  inixp  30195  2reu4a  32148  eelT11  33364  uunT11  33461  uunT11p1  33462  uunT11p2  33463  uun111  33470  bnj594  33838  cdlemg33b  36308
  Copyright terms: Public domain W3C validator