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

Theorem annim 394
 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 392 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 349 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386 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 199  df-an 387 This theorem is referenced by:  pm4.61  395  pm4.52  970  xordi  1002  dfifp6  1052  exanali  1904  sbn  2467  r19.35  3270  difin0ss  4177  ordsssuc2  6064  tfindsg  7338  findsg  7371  isf34lem4  9534  hashfun  13538  isprm5  15823  mdetunilem8  20830  4cycl2vnunb  27698  strlem6  29687  hstrlem6  29695  axacprim  32181  ceqsralv2  32204  dfrdg4  32647  andnand1  32984  relowlpssretop  33807  poimirlem1  34036  poimir  34068  2exanali  39543  limsupre2lem  40864  aifftbifffaibif  42015
 Copyright terms: Public domain W3C validator