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

Theorem annim 407
 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 405 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
21con2bii 361 1 ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  pm4.61  408  pm4.52  982  xordi  1014  dfifp6  1064  exanali  1860  2exanali  1861  sbnOLD  2543  sbnALT  2597  difin0ss  4311  ordsssuc2  6266  tfindsg  7569  findsg  7604  hashfun  13803  isprm5  16049  mdetunilem8  21228  4cycl2vnunb  28078  axacprim  32990  ceqsralv2  33013  dfrdg4  33469  andnand1  33806  relowlpssretop  34726  nlpineqsn  34770  poimirlem1  35003  poimir  35035  limsupre2lem  42292  aifftbifffaibif  43440  nfermltl8rev  44186  nfermltl2rev  44187
 Copyright terms: Public domain W3C validator