Metamath Proof Explorer


Theorem 3bitr2rd

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006)

Ref Expression
Hypotheses 3bitr2d.1 φ ψ χ
3bitr2d.2 φ θ χ
3bitr2d.3 φ θ τ
Assertion 3bitr2rd φ τ ψ

Proof

Step Hyp Ref Expression
1 3bitr2d.1 φ ψ χ
2 3bitr2d.2 φ θ χ
3 3bitr2d.3 φ θ τ
4 1 2 bitr4d φ ψ θ
5 4 3 bitr2d φ τ ψ