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  987  xordi  1019  dfifp6  1069  exanali  1861  2exanali  1862  ceqsralbv  3600  difin0ss  4314  ordsssuc2  6410  tfindsg  7805  findsg  7841  hashfun  14390  isprm5  16668  mdetunilem8  22594  4cycl2vnunb  30375  mxidlirred  33547  axregs  35299  axacprim  35905  dfrdg4  36149  andnand1  36599  relowlpssretop  37694  nlpineqsn  37738  poimirlem1  37956  poimir  37988  fimgmcyc  42993  ralopabb  43856  rexanuz2nf  45938  limsupre2lem  46170  aifftbifffaibif  47381  nfermltl8rev  48230  nfermltl2rev  48231