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  488  xordi  883  exanali  1637  19.35  1654  sbn  2080  rexanali  2751  r19.35  2857  difin0ss  3733  ordsssuc2  4794  tfindsg  6460  findsg  6492  isf34lem4  8534  hashfun  12182  isprm5  13780  mdetunilem8  18266  strlem6  25482  hstrlem6  25490  archiabl  26038  ordtconlem1  26207  axacprim  27204  dfrdg4  27827  andnand1  28091  2exanali  29482  4cycl2vnunb  30452
  Copyright terms: Public domain W3C validator