Metamath Proof Explorer

Theorem bitr

Description: Theorem *4.22 of WhiteheadRussell p. 117. bitri in closed form. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion bitr 
|- ( ( ( ph <-> ps ) /\ ( ps <-> ch ) ) -> ( ph <-> ch ) )

Proof

Step Hyp Ref Expression
1 bibi1 
 |-  ( ( ph <-> ps ) -> ( ( ph <-> ch ) <-> ( ps <-> ch ) ) )
2 1 biimpar 
 |-  ( ( ( ph <-> ps ) /\ ( ps <-> ch ) ) -> ( ph <-> ch ) )