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  6455  tfindsg  7861  findsg  7898  hashfun  14506  isprm5  16804  mdetunilem8  22847  4cycl2vnunb  30778  mxidlirred  33883  axregs  35673  axacprim  36294  dfrdg4  36538  andnand1  37028  relowlpssretop  38126  nlpineqsn  38170  poimirlem1  38378  poimir  38410  fimgmcyc  43424  ralopabb  44259  rexanuz2nf  46328  limsupre2lem  46560  aifftbifffaibif  47817  nfermltl8rev  48666  nfermltl2rev  48667