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

Theorem bibi1 318
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 20 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21bibi1d 311 1  |-  ( (
ph 
<->  ps )  ->  (
( ph  <->  ch )  <->  ( ps  <->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bitr  690  sbeqalb  3205  isclo2  17144  bitr3  28530  sbc3orgVD  28900  trsbcVD  28926  sbcssVD  28932  csbingVD  28933  csbsngVD  28942  csbxpgVD  28943  csbrngVD  28945  csbunigVD  28947  csbfv12gALTVD  28948  e2ebindVD  28961
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 178
  Copyright terms: Public domain W3C validator