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

Theorem bibi1 328
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 22 . 2  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
21bibi1d 320 1  |-  ( (
ph 
<->  ps )  ->  (
( ph  <->  ch )  <->  ( ps  <->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  bitr  713  eqeq1d  2424  sbeqalb  3352  isclo2  20102  bitr3  36837  sbc3orgVD  37220  trsbcVD  37247  sbcssgVD  37253  csbingVD  37254  csbsngVD  37263  csbxpgVD  37264  csbrngVD  37266  csbunigVD  37268  csbfv12gALTVD  37269  e2ebindVD  37282
  Copyright terms: Public domain W3C validator