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

Theorem annim 416
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 415 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 324 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm4.61  417  pm4.52  479  xordi  867  exanali  1596  19.35  1611  sbn  2132  rexanali  2753  r19.35  2857  difin0ss  3696  ordsssuc2  4672  tfindsg  4842  findsg  4874  isf34lem4  8259  hashfun  11702  isprm5  13114  strlem6  23761  hstrlem6  23769  axacprim  25158  dfrdg4  25797  andnand1  26150  2exanali  27565  4cycl2vnunb  28469
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 179  df-an 362
  Copyright terms: Public domain W3C validator