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

Theorem pm5.5 334
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 333 . 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  365  dvelimdf  2081  2sb6rf  2198  elabgt  3240  sbceqal  3376  dffun8  5597  ordiso2  7932  ordtypelem7  7941  cantnf  8103  cantnfOLD  8125  rankonidlem  8237  dfac12lem3  8516  dcomex  8818  indstr2  11161  lublecllem  15820  tsmsgsum  20806  tsmsgsumOLD  20809  tsmsresOLD  20814  tsmsres  20815  tsmsxplem1  20824  caucfil  21891  isarchiofld  28045  wl-nfimf1  30221  pm10.52  31514  tendoeq2  36916  relexp0eq  38239
  Copyright terms: Public domain W3C validator