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

Theorem pm5.5 328
Description: Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm5.5  |-  ( ph  ->  ( ( ph  ->  ps )  <->  ps ) )

Proof of Theorem pm5.5
StepHypRef Expression
1 biimt 327 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
21bicomd 194 1  |-  ( ph  ->  ( ( ph  ->  ps )  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  imim21b  358  elabgt  2886  sbceqal  3017  dffun8  5220  ordiso2  7198  ordtypelem7  7207  cantnf  7363  rankonidlem  7468  dfac12lem3  7739  dcomex  8041  indstr2  10263  lubid  14078  tsmsgsum  17783  tsmsres  17788  tsmsxplem1  17797  caucfil  18671  trant  24315  pm10.52  26927  tendoeq2  30130
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator