Theorem: HTPI.not_imp_not_iff_and (HTPILib/HTPIDefs.lean)

State before:
p q : Prop
⊢ ¬(p → ¬q) ↔ p ∧ q
Tactic:
rw [not_imp, Classical.not_not]
State after:
no goals