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  2050  2sb6rf  2182  elabgt  3247  sbceqal  3387  dffun8  5615  ordiso2  7940  ordtypelem7  7949  cantnf  8112  cantnfOLD  8134  rankonidlem  8246  dfac12lem3  8525  dcomex  8827  indstr2  11160  lublecllem  15475  tsmsgsum  20400  tsmsgsumOLD  20403  tsmsresOLD  20408  tsmsres  20409  tsmsxplem1  20418  caucfil  21485  isarchiofld  27498  wl-nfimf1  29583  pm10.52  30876  tendoeq2  35588
  Copyright terms: Public domain W3C validator