MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  annim Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 iman 401 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 357 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
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  1859  2exanali  1860  ceqsralbv  3657  difin0ss  4373  ordsssuc2  6475  tfindsg  7882  findsg  7919  hashfun  14476  isprm5  16744  mdetunilem8  22625  4cycl2vnunb  30309  mxidlirred  33500  axacprim  35707  dfrdg4  35952  andnand1  36402  relowlpssretop  37365  nlpineqsn  37409  poimirlem1  37628  poimir  37660  fimgmcyc  42544  ralopabb  43424  rexanuz2nf  45503  limsupre2lem  45739  aifftbifffaibif  46933  nfermltl8rev  47729  nfermltl2rev  47730
  Copyright terms: Public domain W3C validator