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  3626  difin0ss  4339  ordsssuc2  6428  tfindsg  7840  findsg  7876  hashfun  14409  isprm5  16684  mdetunilem8  22513  4cycl2vnunb  30226  mxidlirred  33450  axacprim  35701  dfrdg4  35946  andnand1  36396  relowlpssretop  37359  nlpineqsn  37403  poimirlem1  37622  poimir  37654  fimgmcyc  42529  ralopabb  43407  rexanuz2nf  45495  limsupre2lem  45729  aifftbifffaibif  46926  nfermltl8rev  47747  nfermltl2rev  47748