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  3611  difin0ss  4325  ordsssuc2  6410  tfindsg  7803  findsg  7839  hashfun  14360  isprm5  16634  mdetunilem8  22563  4cycl2vnunb  30365  mxidlirred  33553  axregs  35295  axacprim  35901  dfrdg4  36145  andnand1  36595  relowlpssretop  37569  nlpineqsn  37613  poimirlem1  37822  poimir  37854  fimgmcyc  42789  ralopabb  43652  rexanuz2nf  45736  limsupre2lem  45968  aifftbifffaibif  47167  nfermltl8rev  47988  nfermltl2rev  47989