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  1892  2exanali  1893  ceqsralbv  3611  difin0ss  4321  ordsssuc2  6449  tfindsg  7861  findsg  7898  hashfun  14562  isprm5  16863  mdetunilem8  22914  4cycl2vnunb  30873  mxidlirred  33979  axregs  35780  axacprim  36441  dfrdg4  36685  andnand1  37159  relowlpssretop  38255  nlpineqsn  38299  poimirlem1  38507  poimir  38539  fimgmcyc  43560  ralopabb  44370  rexanuz2nf  46446  limsupre2lem  46678  aifftbifffaibif  47935  nfermltl8rev  48784  nfermltl2rev  48785