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

Theorem annim 390
Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
annim ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))

Proof of Theorem annim
StepHypRef Expression
1 iman 388 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 346 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382
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 197  df-an 383
This theorem is referenced by:  pm4.61  391  pm4.52  965  xordi  997  dfifp6  1055  exanali  1937  sbn  2538  r19.35  3232  difin0ss  4093  ordsssuc2  5957  tfindsg  7207  findsg  7240  isf34lem4  9401  hashfun  13426  isprm5  15626  mdetunilem8  20643  4cycl2vnunb  27472  strlem6  29455  hstrlem6  29463  axacprim  31922  ceqsralv2  31945  dfrdg4  32395  andnand1  32735  relowlpssretop  33549  poimirlem1  33743  poimir  33775  2exanali  39113  limsupre2lem  40474  aifftbifffaibif  41608
  Copyright terms: Public domain W3C validator