Theorem annim 403

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm4.61  404  pm4.52  987  xordi  1019  dfifp6  1069  exanali  1861  2exanali  1862  ceqsralbv  3613  difin0ss  4327  ordsssuc2  6418  tfindsg  7813  findsg  7849  hashfun  14372  isprm5  16646  mdetunilem8  22575  4cycl2vnunb  30377  mxidlirred  33564  axregs  35314  axacprim  35920  dfrdg4  36164  andnand1  36614  relowlpssretop  37616  nlpineqsn  37660  poimirlem1  37869  poimir  37901  fimgmcyc  42901  ralopabb  43764  rexanuz2nf  45847  limsupre2lem  46079  aifftbifffaibif  47278  nfermltl8rev  48099  nfermltl2rev  48100