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  985  xordi  1017  dfifp6  1069  exanali  1858  2exanali  1859  ceqsralbv  3670  difin0ss  4396  ordsssuc2  6486  tfindsg  7898  findsg  7937  hashfun  14486  isprm5  16754  mdetunilem8  22646  4cycl2vnunb  30322  mxidlirred  33465  axacprim  35669  dfrdg4  35915  andnand1  36367  relowlpssretop  37330  nlpineqsn  37374  poimirlem1  37581  poimir  37613  fimgmcyc  42489  ralopabb  43373  rexanuz2nf  45408  limsupre2lem  45645  aifftbifffaibif  46836  nfermltl8rev  47616  nfermltl2rev  47617