Theorem annim

Description: Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	annim	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		iman	⊢ ( ( 𝜑 → 𝜓 ) ↔ ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
2	1	con2bii	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ( 𝜑 → 𝜓 ) )