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  3614  difin0ss  4326  ordsssuc2  6404  tfindsg  7801  findsg  7837  hashfun  14362  isprm5  16636  mdetunilem8  22522  4cycl2vnunb  30252  mxidlirred  33422  axregs  35076  axacprim  35682  dfrdg4  35927  andnand1  36377  relowlpssretop  37340  nlpineqsn  37384  poimirlem1  37603  poimir  37635  fimgmcyc  42510  ralopabb  43387  rexanuz2nf  45475  limsupre2lem  45709  aifftbifffaibif  46909  nfermltl8rev  47730  nfermltl2rev  47731