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

Theorem pm5.5 337
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 336 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
21bicomd 204 1  |-  ( ph  ->  ( ( ph  ->  ps )  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  imim21b  368  dvelimdf  2132  2sb6rf  2247  elabgt  3215  sbceqal  3351  dffun8  5624  ordiso2  8032  ordtypelem7  8041  cantnf  8199  rankonidlem  8300  dfac12lem3  8575  dcomex  8877  indstr2  11237  lublecllem  16219  tsmsgsum  21137  tsmsres  21142  tsmsxplem1  21151  caucfil  22237  isarchiofld  28573  wl-nfimf1  31769  tendoeq2  34257  relexp0eq  36150  pm10.52  36569
  Copyright terms: Public domain W3C validator