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  3612  difin0ss  4323  ordsssuc2  6399  tfindsg  7791  findsg  7827  hashfun  14344  isprm5  16618  mdetunilem8  22535  4cycl2vnunb  30268  mxidlirred  33435  axregs  35143  axacprim  35749  dfrdg4  35991  andnand1  36441  relowlpssretop  37404  nlpineqsn  37448  poimirlem1  37667  poimir  37699  fimgmcyc  42573  ralopabb  43450  rexanuz2nf  45536  limsupre2lem  45768  aifftbifffaibif  46958  nfermltl8rev  47779  nfermltl2rev  47780