Theorem annim 404

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 402	. 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
2	1	con2bii 358	1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  pm4.61  405  pm4.52  982  xordi  1014  dfifp6  1066  exanali  1866  2exanali  1867  difin0ss  4308  ordsssuc2  6353  tfindsg  7701  findsg  7740  hashfun  14150  isprm5  16410  mdetunilem8  21766  4cycl2vnunb  28650  axacprim  33644  ceqsralv2  33666  dfrdg4  34249  andnand1  34586  relowlpssretop  35531  nlpineqsn  35575  poimirlem1  35774  poimir  35806  limsupre2lem  43236  aifftbifffaibif  44384  nfermltl8rev  45163  nfermltl2rev  45164