Theorem anidm 396

Description: Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.)

Assertion

Ref	Expression
anidm	⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		pm4.24 395	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))
2	1	bicomi 132	1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑)

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anidmdbi  398  anandi  594  anandir  595  truantru  1446  falanfal  1449  truxortru  1464  truxorfal  1465  falxortru  1466  falxorfal  1467  sbnf2  2034  2eu4  2173  inidm  3418  ralidm  3597  opcom  4349  opeqsn  4351  poirr  4410  rnxpid  5178  xp11m  5182  fununi  5405  brprcneu  5641  erinxp  6821  dom2lem  6988  dmaddpi  7588  dmmulpi  7589  enq0ref  7696  enq0tr  7697  expap0  10877  sqap0  10914  xrmaxiflemcom  11872  gcddvds  12597  isnsg2  13853  eqger  13874  xmeter  15230  clwwlkn2  16345