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

Theorem anidm 642
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 641 . 2  |-  ( ph  <->  (
ph  /\  ph ) )
21bicomi 202 1  |-  ( (
ph  /\  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  anidmdbi  644  anandi  826  anandir  827  nannot  1349  truantru  1423  falanfal  1426  nic-axALT  1521  2eu4OLD  2322  inidm  3634  opcom  4668  opeqsn  4670  poirr  4738  asymref2  5310  xp11  5365  fununi  5575  brprcneu  5780  f13dfv  6097  erinxp  7321  dom2lem  7492  pssnn  7672  dmaddpi  9197  dmmulpi  9198  gcddvds  14174  iscatd2  15107  dfiso2  15197  isnsg2  16367  eqger  16387  gaorber  16482  efgcpbllemb  16909  xmeter  21040  caucfil  21826  axcontlem5  24413  cusgra2v  24604  cusgra3v  24606  erclwwlkref  24955  erclwwlknref  24967  frgra3v  25144  disjunsn  27613  subfaclefac  28845  inixp  30421  2reu4a  32395  eelT11  33871  uunT11  33968  uunT11p1  33969  uunT11p2  33970  uun111  33977  bnj594  34352  cdlemg33b  36881
  Copyright terms: Public domain W3C validator