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  826  anandir  827  nannot  1349  truantru  1403  falanfal  1406  nic-axALT  1491  sbnf2OLD  2167  2eu4OLD  2391  inidm  3707  opcom  4741  opeqsn  4743  poirr  4811  asymref2  5382  xp11  5440  fununi  5652  brprcneu  5857  f13dfv  6166  erinxp  7382  dom2lem  7552  pssnn  7735  dmaddpi  9264  dmmulpi  9265  gcddvds  14005  iscatd2  14929  isnsg2  16023  eqger  16043  gaorber  16138  efgcpbllemb  16566  xmeter  20668  caucfil  21454  axcontlem5  23944  cusgra2v  24135  cusgra3v  24137  erclwwlkref  24486  erclwwlknref  24498  frgra3v  24675  disjunsn  27123  subfaclefac  28257  inixp  29820  2reu4a  31661  eelT11  32576  uunT11  32673  uunT11p1  32674  uunT11p2  32675  uun111  32682  bnj594  33049  cdlemg33b  35503
  Copyright terms: Public domain W3C validator