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

Theorem annim 402
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 400 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 356 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394
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 206  df-an 395
This theorem is referenced by:  pm4.61  403  pm4.52  982  xordi  1014  dfifp6  1066  exanali  1854  2exanali  1855  ceqsralbv  3645  difin0ss  4372  ordsssuc2  6465  tfindsg  7871  findsg  7911  hashfun  14436  isprm5  16685  mdetunilem8  22541  4cycl2vnunb  30120  mxidlirred  33210  axacprim  35334  dfrdg4  35580  andnand1  35918  relowlpssretop  36876  nlpineqsn  36920  poimirlem1  37127  poimir  37159  ralopabb  42872  rexanuz2nf  44904  limsupre2lem  45141  aifftbifffaibif  46332  nfermltl8rev  47111  nfermltl2rev  47112
  Copyright terms: Public domain W3C validator