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

Theorem annim 423
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 422 . 2  |-  ( (
ph  ->  ps )  <->  -.  ( ph  /\  -.  ps )
)
21con2bii 330 1  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  pm4.61  424  pm4.52  489  xordi  896  dfifp6  1392  exanali  1691  19.35OLD  1709  sbn  2156  rexanaliOLD  2912  r19.35  2954  difin0ss  3838  ordsssuc2  5498  tfindsg  6678  findsg  6711  isf34lem4  8789  hashfun  12544  isprm5  14462  mdetunilem8  19413  4cycl2vnunb  25434  strlem6  27588  hstrlem6  27596  axacprim  29908  dfrdg4  30289  andnand1  30631  relowlpssretop  31281  2exanali  36141
  Copyright terms: Public domain W3C validator