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  986  xordi  1018  dfifp6  1068  exanali  1857  2exanali  1858  ceqsralbv  3657  difin0ss  4379  ordsssuc2  6477  tfindsg  7882  findsg  7920  hashfun  14473  isprm5  16741  mdetunilem8  22641  4cycl2vnunb  30319  mxidlirred  33480  axacprim  35687  dfrdg4  35933  andnand1  36384  relowlpssretop  37347  nlpineqsn  37391  poimirlem1  37608  poimir  37640  fimgmcyc  42521  ralopabb  43401  rexanuz2nf  45443  limsupre2lem  45680  aifftbifffaibif  46871  nfermltl8rev  47667  nfermltl2rev  47668
  Copyright terms: Public domain W3C validator