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  1032  dfifp6  1082  exanali  1882  2exanali  1883  ceqsralbv  3619  difin0ss  4329  ordsssuc2  6443  tfindsg  7845  findsg  7882  hashfun  14462  isprm5  16754  mdetunilem8  22733  4cycl2vnunb  30546  mxidlirred  33667  axregs  35442  axacprim  36065  dfrdg4  36309  andnand1  36769  relowlpssretop  37865  nlpineqsn  37909  poimirlem1  38127  poimir  38159  fimgmcyc  43159  ralopabb  43994  rexanuz2nf  46065  limsupre2lem  46297  aifftbifffaibif  47514  nfermltl8rev  48363  nfermltl2rev  48364