Metamath Proof Explorer

Theorem bitr4i

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypotheses bitr4i.1 
|- ( ph <-> ps )
bitr4i.2 
|- ( ch <-> ps )
Assertion bitr4i 
|- ( ph <-> ch )

Proof

Step Hyp Ref Expression
1 bitr4i.1 
 |-  ( ph <-> ps )
2 bitr4i.2 
 |-  ( ch <-> ps )
3 2 bicomi 
 |-  ( ps <-> ch )
4 1 3 bitri 
 |-  ( ph <-> ch )