Theorem annim 409

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm4.61  410  pm4.52  1000  xordi  1034  dfifp6  1084  exanali  1891  2exanali  1892  ceqsralbv  3610  difin0ss  4320  ordsssuc2  6456  tfindsg  7873  findsg  7910  hashfun  14586  isprm5  16889  mdetunilem8  22940  4cycl2vnunb  30897  mxidlirred  34044  axregs  35864  axacprim  36565  dfrdg4  36808  andnand1  37282  relowlpssretop  38381  nlpineqsn  38425  poimirlem1  38633  poimir  38665  fimgmcyc  43692  ralopabb  44506  rexanuz2nf  46596  limsupre2lem  46828  aifftbifffaibif  48085  nfermltl8rev  48934  nfermltl2rev  48935