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

Theorem annim 425
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 424 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 332 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  pm4.61  426  pm4.52  491  xordi  893  exanali  1647  19.35OLD  1665  sbn  2105  rexanaliOLD  2967  r19.35  3008  difin0ss  3893  ordsssuc2  4966  tfindsg  6673  findsg  6705  isf34lem4  8753  hashfun  12455  isprm5  14105  mdetunilem8  18885  4cycl2vnunb  24690  strlem6  26848  hstrlem6  26856  archiabl  27401  ordtconlem1  27539  axacprim  28551  dfrdg4  29174  andnand1  29438  2exanali  30871  limcrecl  31171  bj-dfif6  33231
  Copyright terms: Public domain W3C validator