Metamath Proof Explorer

Theorem 3bitr4i

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypotheses 3bitr4i.1 φ ψ
3bitr4i.2 χ φ
3bitr4i.3 θ ψ
Assertion 3bitr4i χ θ


Step Hyp Ref Expression
1 3bitr4i.1 φ ψ
2 3bitr4i.2 χ φ
3 3bitr4i.3 θ ψ
4 1 3 bitr4i φ θ
5 2 4 bitri χ θ