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  2848  sbceqal  2972  dffun8  5139  ordiso2  7114  ordtypelem7  7123  cantnf  7279  rankonidlem  7384  dfac12lem3  7655  dcomex  7957  indstr2  10175  lubid  13960  tsmsgsum  17653  tsmsres  17658  tsmsxplem1  17667  caucfil  18541  trant  24114  pm10.52  26726  tendoeq2  29764
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