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  3619  difin0ss  4331  ordsssuc2  6461  tfindsg  7866  findsg  7903  hashfun  14494  isprm5  16791  mdetunilem8  22813  4cycl2vnunb  30678  mxidlirred  33786  axregs  35576  axacprim  36220  dfrdg4  36464  andnand1  36953  relowlpssretop  38051  nlpineqsn  38095  poimirlem1  38313  poimir  38345  fimgmcyc  43343  ralopabb  44178  rexanuz2nf  46247  limsupre2lem  46479  aifftbifffaibif  47699  nfermltl8rev  48548  nfermltl2rev  48549