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

Theorem pm5.5 336
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 335 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
21bicomd 201 1  |-  ( ph  ->  ( ( ph  ->  ps )  <->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  imim21b  367  dvelimdf  2027  2sb6rf  2160  elabgt  3101  sbceqal  3240  dffun8  5443  ordiso2  7727  ordtypelem7  7736  cantnf  7899  cantnfOLD  7921  rankonidlem  8033  dfac12lem3  8312  dcomex  8614  indstr2  10931  lublecllem  15156  tsmsgsum  19707  tsmsgsumOLD  19710  tsmsresOLD  19715  tsmsres  19716  tsmsxplem1  19725  caucfil  20792  isarchiofld  26283  wl-nfimf1  28351  pm10.52  29614  tendoeq2  34415
  Copyright terms: Public domain W3C validator