Theorem annim 404

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm4.61  405  pm4.52  992  xordi  1024  dfifp6  1074  exanali  1866  2exanali  1867  ceqsralbv  3602  difin0ss  4308  ordsssuc2  6410  tfindsg  7808  findsg  7844  hashfun  14397  isprm5  16675  mdetunilem8  22609  4cycl2vnunb  30385  mxidlirred  33562  axregs  35327  axacprim  35942  dfrdg4  36186  andnand1  36636  relowlpssretop  37733  nlpineqsn  37777  poimirlem1  37995  poimir  38027  fimgmcyc  43027  ralopabb  43862  rexanuz2nf  45942  limsupre2lem  46174  aifftbifffaibif  47391  nfermltl8rev  48240  nfermltl2rev  48241