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  3614  difin0ss  4324  ordsssuc2  6477  tfindsg  7899  findsg  7936  hashfun  14612  isprm5  16915  mdetunilem8  22967  4cycl2vnunb  30924  mxidlirred  34081  axregs  35920  axacprim  36663  dfrdg4  36906  andnand1  37380  relowlpssretop  38492  nlpineqsn  38536  poimirlem1  38744  poimir  38776  fimgmcyc  43802  ralopabb  44615  rexanuz2nf  46717  limsupre2lem  46949  aifftbifffaibif  48206  nfermltl8rev  49055  nfermltl2rev  49056