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  2987  isclo2  16752  bitr3  27288  sbc3orgVD  27640  trsbcVD  27666  sbcssVD  27672  csbingVD  27673  csbsngVD  27682  csbxpgVD  27683  csbrngVD  27685  csbunigVD  27687  csbfv12gALTVD  27688  e2ebindVD  27701
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