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

Theorem bibi1 319
Description: Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
bibi1  |-  ( (
ph 
<->  ps )  ->  (
( ph  <->  ch )  <->  ( ps  <->  ch ) ) )

Proof of Theorem bibi1
StepHypRef Expression
1 id 21 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21bibi1d 312 1  |-  ( (
ph 
<->  ps )  ->  (
( ph  <->  ch )  <->  ( ps  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  bitr  692  sbeqalb  3018  isclo2  16788  bitr3  27408  sbc3orgVD  27760  trsbcVD  27786  sbcssVD  27792  csbingVD  27793  csbsngVD  27802  csbxpgVD  27803  csbrngVD  27805  csbunigVD  27807  csbfv12gALTVD  27808  e2ebindVD  27821
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