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

Theorem annim 426
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 425 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 333 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm4.61  427  pm4.52  493  xordi  903  dfifp6  1426  exanali  1715  sbn  2189  rexanaliOLD  2930  r19.35  2972  difin0ss  3863  ordsssuc2  5530  tfindsg  6701  findsg  6734  isf34lem4  8814  hashfun  12613  isprm5  14650  mdetunilem8  19642  4cycl2vnunb  25743  strlem6  27907  hstrlem6  27915  axacprim  30342  dfrdg4  30723  andnand1  31064  relowlpssretop  31731  poimirlem1  31905  poimir  31937  2exanali  36707  aifftbifffaibif  38380
  Copyright terms: Public domain W3C validator