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  890  exanali  1638  19.35OLD  1656  sbn  2091  rexanali  2877  r19.35  2967  difin0ss  3848  ordsssuc2  4910  tfindsg  6576  findsg  6608  isf34lem4  8652  hashfun  12312  isprm5  13911  mdetunilem8  18552  strlem6  25807  hstrlem6  25815  archiabl  26355  ordtconlem1  26494  axacprim  27497  dfrdg4  28120  andnand1  28384  2exanali  29783  4cycl2vnunb  30752  bj-dfif6  32400
  Copyright terms: Public domain W3C validator