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

Theorem annim 404
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 402 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 359 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  pm4.61  405  pm4.52  978  xordi  1010  dfifp6  1060  exanali  1850  2exanali  1851  sbnOLD  2537  sbnALT  2591  difin0ss  4327  ordsssuc2  6273  tfindsg  7563  findsg  7597  hashfun  13788  isprm5  16041  mdetunilem8  21158  4cycl2vnunb  27997  axacprim  32831  ceqsralv2  32854  dfrdg4  33310  andnand1  33647  relowlpssretop  34528  nlpineqsn  34572  poimirlem1  34775  poimir  34807  limsupre2lem  41885  aifftbifffaibif  43038  nfermltl8rev  43754  nfermltl2rev  43755
  Copyright terms: Public domain W3C validator