Theorem annim 406

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm4.61  407  pm4.52  981  xordi  1013  dfifp6  1063  exanali  1855  2exanali  1856  sbnOLD  2537  sbnALT  2591  difin0ss  4327  ordsssuc2  6273  tfindsg  7569  findsg  7603  hashfun  13792  isprm5  16045  mdetunilem8  21222  4cycl2vnunb  28063  axacprim  32928  ceqsralv2  32951  dfrdg4  33407  andnand1  33744  relowlpssretop  34639  nlpineqsn  34683  poimirlem1  34887  poimir  34919  limsupre2lem  41998  aifftbifffaibif  43151  nfermltl8rev  43901  nfermltl2rev  43902