Theorem annim 441

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

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

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 386

This theorem is referenced by:  pm4.61  442  pm4.52  512  xordi  937  dfifp6  1018  exanali  1785  sbn  2390  r19.35  3082  difin0ss  3944  ordsssuc2  5812  tfindsg  7057  findsg  7090  isf34lem4  9196  hashfun  13219  isprm5  15413  mdetunilem8  20419  4cycl2vnunb  27147  strlem6  29099  hstrlem6  29107  axacprim  31569  ceqsralv2  31593  dfrdg4  32042  andnand1  32382  relowlpssretop  33192  poimirlem1  33390  poimir  33422  2exanali  38413  limsupre2lem  39762  aifftbifffaibif  40857