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

Theorem annim 415
Description: Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
annim  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )

Proof of Theorem annim
StepHypRef Expression
1 iman 414 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 323 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm4.61  416  pm4.52  478  xordi  866  exanali  1592  19.35  1607  rexanali  2697  r19.35  2800  difin0ss  3639  ordsssuc2  4612  tfindsg  4782  findsg  4814  isf34lem4  8192  hashfun  11629  isprm5  13041  strlem6  23609  hstrlem6  23617  axacprim  24937  dfrdg4  25515  andnand1  25864  2exanali  27257  4cycl2vnunb  27772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator