Metamath Proof Explorer


Theorem 3bitr4ri

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995)

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

Proof

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