Metamath Proof Explorer

Theorem bitr3

Description: Closed nested implication form of bitr3i . Derived automatically from bitr3VD . (Contributed by Alan Sare, 31-Dec-2011)

Ref Expression
Assertion bitr3 
|- ( ( ph <-> ps ) -> ( ( ph <-> ch ) -> ( ps <-> ch ) ) )

Proof

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