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  1575  19.35  1590  rexanali  2602  r19.35  2700  difin0ss  3533  ordsssuc2  4497  tfindsg  4667  findsg  4699  isf34lem4  8019  hashfun  11405  isprm5  12807  strlem6  22852  hstrlem6  22860  axacprim  24068  dfrdg4  24559  andnand1  24908  2exanali  27688  4cycl2vnunb  28438  a12studyALT  29755
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