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

Theorem annim 431
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 430 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 338 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 377
This theorem is referenced by:  pm4.61  432  pm4.52  498  xordi  909  dfifp6  1434  exanali  1725  sbn  2221  r19.35  2905  difin0ss  3801  ordsssuc2  5490  tfindsg  6675  findsg  6708  isf34lem4  8794  hashfun  12604  isprm5  14662  mdetunilem8  19655  4cycl2vnunb  25757  strlem6  27921  hstrlem6  27929  axacprim  30340  ceqsralv2  30364  dfrdg4  30724  andnand1  31065  relowlpssretop  31769  poimirlem1  31943  poimir  31975  2exanali  36738  aifftbifffaibif  38600
  Copyright terms: Public domain W3C validator