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

Theorem annim 425
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 424 . 2
21con2bii 332 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  pm4.61  426  pm4.52  491  xordi  895  dfifp6  1386  exanali  1670  19.35OLD  1688  sbn  2132  rexanaliOLD  2962  r19.35  3004  difin0ss  3894  ordsssuc2  4971  tfindsg  6695  findsg  6727  isf34lem4  8778  hashfun  12495  isprm5  14253  mdetunilem8  19121  4cycl2vnunb  25017  strlem6  27175  hstrlem6  27183  axacprim  29079  dfrdg4  29600  andnand1  29864  2exanali  31293
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 185  df-an 371
  Copyright terms: Public domain W3C validator