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  1860  2exanali  1861  ceqsralbv  3608  difin0ss  4322  ordsssuc2  6406  tfindsg  7799  findsg  7835  hashfun  14348  isprm5  16622  mdetunilem8  22537  4cycl2vnunb  30274  mxidlirred  33446  axregs  35168  axacprim  35774  dfrdg4  36018  andnand1  36468  relowlpssretop  37431  nlpineqsn  37475  poimirlem1  37684  poimir  37716  fimgmcyc  42655  ralopabb  43531  rexanuz2nf  45617  limsupre2lem  45849  aifftbifffaibif  47048  nfermltl8rev  47869  nfermltl2rev  47870