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

Theorem annim 440
 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 439 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 346 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  pm4.61  441  pm4.52  511  xordi  935  dfifp6  1012  exanali  1773  sbn  2379  r19.35  3065  difin0ss  3900  ordsssuc2  5731  tfindsg  6952  findsg  6985  isf34lem4  9082  hashfun  13084  isprm5  15257  mdetunilem8  20244  4cycl2vnunb  26544  strlem6  28499  hstrlem6  28507  axacprim  30838  ceqsralv2  30862  dfrdg4  31228  andnand1  31568  relowlpssretop  32388  poimirlem1  32580  poimir  32612  2exanali  37609  aifftbifffaibif  39737  4cycl2vnunb-av  41460
 Copyright terms: Public domain W3C validator