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 φ ψ χ ψ φ χ


Step Hyp Ref Expression
1 id χ ψ χ ψ
2 1 bibi2d χ ψ φ χ φ ψ
3 2 biimparc φ ψ χ ψ φ χ