Theorem annim 402

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

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

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 395

This theorem is referenced by:  pm4.61  403  pm4.52  982  xordi  1014  dfifp6  1066  exanali  1854  2exanali  1855  ceqsralbv  3645  difin0ss  4372  ordsssuc2  6465  tfindsg  7871  findsg  7911  hashfun  14436  isprm5  16685  mdetunilem8  22541  4cycl2vnunb  30120  mxidlirred  33210  axacprim  35334  dfrdg4  35580  andnand1  35918  relowlpssretop  36876  nlpineqsn  36920  poimirlem1  37127  poimir  37159  ralopabb  42872  rexanuz2nf  44904  limsupre2lem  45141  aifftbifffaibif  46332  nfermltl8rev  47111  nfermltl2rev  47112