Theorem annim 394

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 392	. 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
2	1	con2bii 349	1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pm4.61  395  pm4.52  970  xordi  1002  dfifp6  1052  exanali  1904  sbn  2467  r19.35  3270  difin0ss  4177  ordsssuc2  6064  tfindsg  7338  findsg  7371  isf34lem4  9534  hashfun  13538  isprm5  15823  mdetunilem8  20830  4cycl2vnunb  27698  strlem6  29687  hstrlem6  29695  axacprim  32181  ceqsralv2  32204  dfrdg4  32647  andnand1  32984  relowlpssretop  33807  poimirlem1  34036  poimir  34068  2exanali  39543  limsupre2lem  40864  aifftbifffaibif  42015