Theorem annim 440

Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
annim	⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))

Proof of Theorem annim

Step	Hyp	Ref	Expression
1		iman 439	. 2 ⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
2	1	con2bii 346	1 ⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm4.61  441  pm4.52  511  xordi  935  dfifp6  1012  exanali  1773  sbn  2379  r19.35  3065  difin0ss  3900  ordsssuc2  5731  tfindsg  6952  findsg  6985  isf34lem4  9082  hashfun  13084  isprm5  15257  mdetunilem8  20244  4cycl2vnunb  26544  strlem6  28499  hstrlem6  28507  axacprim  30838  ceqsralv2  30862  dfrdg4  31228  andnand1  31568  relowlpssretop  32388  poimirlem1  32580  poimir  32612  2exanali  37609  aifftbifffaibif  39737  4cycl2vnunb-av  41460