Rule_of_Idempotence
Provedconjunctiondisjunctionproofwiki
The rule of idempotence: (p and p) iff p, and (p or p) iff p.
Preamble
import Mathlib.Tactic
Formal statement
theorem Rule_of_Idempotence (p : Prop) : (p ∧ p ↔ p) ∧ (p ∨ p ↔ p) := by sorry
Source