Theorem annim 390

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  pm4.61  391  pm4.52  965  xordi  997  dfifp6  1055  exanali  1937  sbn  2538  r19.35  3232  difin0ss  4093  ordsssuc2  5957  tfindsg  7207  findsg  7240  isf34lem4  9401  hashfun  13426  isprm5  15626  mdetunilem8  20643  4cycl2vnunb  27472  strlem6  29455  hstrlem6  29463  axacprim  31922  ceqsralv2  31945  dfrdg4  32395  andnand1  32735  relowlpssretop  33549  poimirlem1  33743  poimir  33775  2exanali  39113  limsupre2lem  40474  aifftbifffaibif  41608