Theorem annim 404

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  pm4.61  405  pm4.52  982  xordi  1014  dfifp6  1066  exanali  1862  2exanali  1863  difin0ss  4302  ordsssuc2  6354  tfindsg  7707  findsg  7746  hashfun  14152  isprm5  16412  mdetunilem8  21768  4cycl2vnunb  28654  axacprim  33648  ceqsralv2  33670  dfrdg4  34253  andnand1  34590  relowlpssretop  35535  nlpineqsn  35579  poimirlem1  35778  poimir  35810  limsupre2lem  43265  aifftbifffaibif  44416  nfermltl8rev  45194  nfermltl2rev  45195