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  981  xordi  1013  dfifp6  1065  exanali  1860  2exanali  1861  ceqsralbv  3646  difin0ss  4369  ordsssuc2  6456  tfindsg  7854  findsg  7894  hashfun  14403  isprm5  16650  mdetunilem8  22343  4cycl2vnunb  29808  mxidlirred  32860  axacprim  34978  dfrdg4  35225  andnand1  35591  relowlpssretop  36550  nlpineqsn  36594  poimirlem1  36794  poimir  36826  ralopabb  42466  rexanuz2nf  44503  limsupre2lem  44740  aifftbifffaibif  45931  nfermltl8rev  46710  nfermltl2rev  46711