Theorem annim 408

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm4.61  409  pm4.52  1000  xordi  1034  dfifp6  1084  exanali  1889  2exanali  1890  ceqsralbv  3617  difin0ss  4329  ordsssuc2  6456  tfindsg  7858  findsg  7895  hashfun  14476  isprm5  16767  mdetunilem8  22757  4cycl2vnunb  30622  mxidlirred  33736  axregs  35533  axacprim  36180  dfrdg4  36424  andnand1  36893  relowlpssretop  37991  nlpineqsn  38035  poimirlem1  38253  poimir  38285  fimgmcyc  43285  ralopabb  44120  rexanuz2nf  46189  limsupre2lem  46421  aifftbifffaibif  47641  nfermltl8rev  48490  nfermltl2rev  48491