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

Theorem pm5.5 327
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 326 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
21bicomd 193 1  |-  ( ph  ->  ( ( ph  ->  ps )  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  imim21b  357  dvelimdf  2066  elabgt  3071  sbceqal  3204  dffun8  5472  ordiso2  7476  ordtypelem7  7485  cantnf  7641  rankonidlem  7746  dfac12lem3  8017  dcomex  8319  indstr2  10546  lubid  14431  tsmsgsum  18160  tsmsres  18165  tsmsxplem1  18174  caucfil  19228  pm10.52  27528  tendoeq2  31508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator