Metamath Proof Explorer

Theorem bitr2i

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

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

Proof

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