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  2862  sbceqal  2986  dffun8  5185  ordiso2  7163  ordtypelem7  7172  cantnf  7328  rankonidlem  7433  dfac12lem3  7704  dcomex  8006  indstr2  10228  lubid  14043  tsmsgsum  17748  tsmsres  17753  tsmsxplem1  17762  caucfil  18636  trant  24280  pm10.52  26892  tendoeq2  30093
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