Theorem anidm 478

Description: Idempotent law for conjunction.

Assertion

Ref	Expression
anidm	|- ((ph /\ ph) <-> ph)

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		simpl 346	. 2 |- ((ph /\ ph) -> ph)
2		pm3.2 305	. . 3 |- (ph -> (ph -> (ph /\ ph)))
3	2	pm2.43i 78	. 2 |- (ph -> (ph /\ ph))
4	1, 3	impbii 174	1 |- ((ph /\ ph) <-> ph)

Syntax hints:   <-> wb 163   /\ wa 240

This theorem is referenced by:  pm4.24 479  anidmdbi 481  anandi 568  anandir 569  nic-justneg 1233  nic-axALT 1240  2eu4 1856  inidm 2803  ralsn 3084  opcom 3547  opeqsn 3549  poirr 3597  eufromeq2 3829  eufromeq6 3833  asymref2 4310  asymref2OLD 4311  xp11 4347  fununi 4481  finOLD 4594  th3qlem1 5373  dom2d 5463  pssnn 5628  dmaddpi 6170  dmmulpi 6171  lt2msqi 7064  cau3iri 8167  hlimcauii 10739  bnj594 13300  gcddvds 13722  TTAid 14106  FFAid 14109  fneerdm 15498  inixp 15722  erreft 16259  grpclNEW 17106  ringclNEW 17144

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain