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  937  dfifp6  1018  exanali  1785  sbn  2390  r19.35  3082  difin0ss  3944  ordsssuc2  5812  tfindsg  7057  findsg  7090  isf34lem4  9196  hashfun  13219  isprm5  15413  mdetunilem8  20419  4cycl2vnunb  27147  strlem6  29099  hstrlem6  29107  axacprim  31569  ceqsralv2  31593  dfrdg4  32042  andnand1  32382  relowlpssretop  33192  poimirlem1  33390  poimir  33422  2exanali  38413  limsupre2lem  39762  aifftbifffaibif  40857
 Copyright terms: Public domain W3C validator