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

Theorem pm5.5 326
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 325 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
21bicomd 192 1  |-  ( ph  ->  ( ( ph  ->  ps )  <->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imim21b  356  elabgt  2924  sbceqal  3055  dffun8  5297  ordiso2  7246  ordtypelem7  7255  cantnf  7411  rankonidlem  7516  dfac12lem3  7787  dcomex  8089  indstr2  10312  lubid  14132  tsmsgsum  17837  tsmsres  17842  tsmsxplem1  17851  caucfil  18725  trant  25052  pm10.52  27663  tendoeq2  31585
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 177
  Copyright terms: Public domain W3C validator