Theorem annim 407

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm4.61  408  pm4.52  997  xordi  1029  dfifp6  1079  exanali  1878  2exanali  1879  ceqsralbv  3615  difin0ss  4323  ordsssuc2  6433  tfindsg  7835  findsg  7872  hashfun  14443  isprm5  16732  mdetunilem8  22666  4cycl2vnunb  30448  mxidlirred  33620  axregs  35395  axacprim  36017  dfrdg4  36261  andnand1  36721  relowlpssretop  37818  nlpineqsn  37862  poimirlem1  38080  poimir  38112  fimgmcyc  43112  ralopabb  43947  rexanuz2nf  46026  limsupre2lem  46258  aifftbifffaibif  47475  nfermltl8rev  48324  nfermltl2rev  48325