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

Theorem annim 441
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 440 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 347 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  pm4.61  442  pm4.52  512  xordi  936  dfifp6  1017  exanali  1783  sbn  2390  r19.35  3077  difin0ss  3925  ordsssuc2  5778  tfindsg  7014  findsg  7047  isf34lem4  9150  hashfun  13171  isprm5  15350  mdetunilem8  20353  4cycl2vnunb  27031  strlem6  28982  hstrlem6  28990  axacprim  31319  ceqsralv2  31343  dfrdg4  31727  andnand1  32067  relowlpssretop  32871  poimirlem1  33069  poimir  33101  2exanali  38096  limsupre2lem  39383  aifftbifffaibif  40413
  Copyright terms: Public domain W3C validator