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  3623  difin0ss  4336  ordsssuc2  6425  tfindsg  7837  findsg  7873  hashfun  14402  isprm5  16677  mdetunilem8  22506  4cycl2vnunb  30219  mxidlirred  33443  axacprim  35694  dfrdg4  35939  andnand1  36389  relowlpssretop  37352  nlpineqsn  37396  poimirlem1  37615  poimir  37647  fimgmcyc  42522  ralopabb  43400  rexanuz2nf  45488  limsupre2lem  45722  aifftbifffaibif  46922  nfermltl8rev  47743  nfermltl2rev  47744