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  3599  difin0ss  4313  ordsssuc2  6416  tfindsg  7812  findsg  7848  hashfun  14399  isprm5  16677  mdetunilem8  22584  4cycl2vnunb  30360  mxidlirred  33532  axregs  35283  axacprim  35889  dfrdg4  36133  andnand1  36583  relowlpssretop  37680  nlpineqsn  37724  poimirlem1  37942  poimir  37974  fimgmcyc  42979  ralopabb  43838  rexanuz2nf  45920  limsupre2lem  46152  aifftbifffaibif  47369  nfermltl8rev  48218  nfermltl2rev  48219