Theorem: ClassicalPropositionalLogic.isTrue_equiv (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
⊢ IsTrue v (A ⇔ B) ↔ (IsTrue v A ↔ IsTrue v B)
Tactic:
simp
State after:
v : Variable → Prop
A B : Formula
⊢ (IsTrue v A → IsTrue v B) ∧ (IsTrue v B → IsTrue v A) ↔ (IsTrue v A ↔ IsTrue v B)

State before:
v : Variable → Prop
A B : Formula
⊢ (IsTrue v A → IsTrue v B) ∧ (IsTrue v B → IsTrue v A) ↔ (IsTrue v A ↔ IsTrue v B)
Tactic:
tauto
State after:
no goals