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

Theorem anidm 649
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 648 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 206 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  anidmdbi  651  anandi  836  anandir  837  nannot  1388  truantru  1462  falanfal  1465  nic-axALT  1554  inidm  3672  opcom  4712  opeqsn  4714  poirr  4783  asymref2  5234  xp11  5289  fununi  5665  brprcneu  5872  f13dfv  6186  erinxp  7443  dom2lem  7614  pssnn  7794  dmaddpi  9317  dmmulpi  9318  gcddvds  14470  iscatd2  15580  dfiso2  15670  isnsg2  16840  eqger  16860  gaorber  16955  efgcpbllemb  17398  xmeter  21440  caucfil  22245  tgcgr4  24568  axcontlem5  24990  cusgra2v  25182  cusgra3v  25184  erclwwlkref  25533  erclwwlknref  25545  frgra3v  25722  disjunsn  28200  bnj594  29725  subfaclefac  29901  isbasisrelowllem1  31716  isbasisrelowllem2  31717  inixp  32013  cdlemg33b  34237  eelT11  36992  uunT11  37088  uunT11p1  37089  uunT11p2  37090  uun111  37097  2reu4a  38367
  Copyright terms: Public domain W3C validator