Metamath Proof Explorer

Theorem biantr

Description: A transitive law of equivalence. Compare Theorem *4.22 of WhiteheadRussell p. 117. (Contributed by NM, 18-Aug-1993)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( ch <-> ps ) -> ( ch <-> ps ) )
2 1 bibi2d 
 |-  ( ( ch <-> ps ) -> ( ( ph <-> ch ) <-> ( ph <-> ps ) ) )
3 2 biimparc 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> ps ) ) -> ( ph <-> ch ) )