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

Theorem annim 414
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 413 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 322 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm4.61  415  pm4.52  477  xordi  865  exanali  1572  19.35  1587  rexanali  2589  r19.35  2687  difin0ss  3520  ordsssuc2  4481  tfindsg  4651  findsg  4683  isf34lem4  8003  hashfun  11389  isprm5  12791  strlem6  22836  hstrlem6  22844  axacprim  24053  dfrdg4  24488  andnand1  24837  2exanali  27586  a12studyALT  29133
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 177  df-an 360
  Copyright terms: Public domain W3C validator