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  2712  r19.35  2815  difin0ss  3654  ordsssuc2  4629  tfindsg  4799  findsg  4831  isf34lem4  8213  hashfun  11655  isprm5  13067  strlem6  23712  hstrlem6  23720  axacprim  25109  dfrdg4  25703  andnand1  26052  2exanali  27454  4cycl2vnunb  28121
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