Theorem annim 403

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

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

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 396

This theorem is referenced by:  pm4.61  404  pm4.52  981  xordi  1013  dfifp6  1065  exanali  1863  2exanali  1864  difin0ss  4299  ordsssuc2  6339  tfindsg  7682  findsg  7720  hashfun  14080  isprm5  16340  mdetunilem8  21676  4cycl2vnunb  28555  axacprim  33548  ceqsralv2  33572  dfrdg4  34180  andnand1  34517  relowlpssretop  35462  nlpineqsn  35506  poimirlem1  35705  poimir  35737  limsupre2lem  43155  aifftbifffaibif  44303  nfermltl8rev  45082  nfermltl2rev  45083