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  1339  truantru  1393  falanfal  1396  nic-axALT  1481  sbnf2OLD  2145  2eu4OLD  2365  inidm  3554  opcom  4580  opeqsn  4582  poirr  4647  asymref2  5210  xp11  5268  fununi  5479  brprcneu  5679  erinxp  7166  dom2lem  7341  pssnn  7523  dmaddpi  9051  dmmulpi  9052  gcddvds  13691  iscatd2  14611  isnsg2  15702  eqger  15722  gaorber  15817  efgcpbllemb  16243  xmeter  19988  caucfil  20774  axcontlem5  23182  cusgra2v  23338  cusgra3v  23340  disjunsn  25904  subfaclefac  27033  inixp  28593  2reu4a  29984  f13dfv  30118  erclwwlkref  30454  erclwwlknref  30470  frgra3v  30565  eelT11  31361  uunT11  31458  uunT11p1  31459  uunT11p2  31460  uun111  31467  bnj594  31834  cdlemg33b  34244
  Copyright terms: Public domain W3C validator