Theorem annim 403

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm4.61  404  pm4.52  986  xordi  1018  dfifp6  1068  exanali  1859  2exanali  1860  ceqsralbv  3636  difin0ss  4348  ordsssuc2  6445  tfindsg  7856  findsg  7893  hashfun  14455  isprm5  16726  mdetunilem8  22557  4cycl2vnunb  30271  mxidlirred  33487  axacprim  35724  dfrdg4  35969  andnand1  36419  relowlpssretop  37382  nlpineqsn  37426  poimirlem1  37645  poimir  37677  fimgmcyc  42557  ralopabb  43435  rexanuz2nf  45519  limsupre2lem  45753  aifftbifffaibif  46950  nfermltl8rev  47756  nfermltl2rev  47757