Theorem annim 407

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

Assertion

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

Proof of Theorem annim

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  pm4.61  408  pm4.52  982  xordi  1014  dfifp6  1064  exanali  1860  2exanali  1861  sbnALT  2571  difin0ss  4282  ordsssuc2  6247  tfindsg  7555  findsg  7590  hashfun  13794  isprm5  16041  mdetunilem8  21224  4cycl2vnunb  28075  axacprim  33046  ceqsralv2  33069  dfrdg4  33525  andnand1  33862  relowlpssretop  34781  nlpineqsn  34825  poimirlem1  35058  poimir  35090  limsupre2lem  42366  aifftbifffaibif  43514  nfermltl8rev  44260  nfermltl2rev  44261