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

Theorem bibi1 317
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 19 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21bibi1d 310 1  |-  ( (
ph 
<->  ps )  ->  (
( ph  <->  ch )  <->  ( ps  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bitr  689  sbeqalb  3056  isclo2  16841  bitr3  28571  sbc3orgVD  28943  trsbcVD  28969  sbcssVD  28975  csbingVD  28976  csbsngVD  28985  csbxpgVD  28986  csbrngVD  28988  csbunigVD  28990  csbfv12gALTVD  28991  e2ebindVD  29004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator