Metamath Proof Explorer


Theorem 3bitr4rd

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

Ref Expression
Hypotheses 3bitr4d.1 φ ψ χ
3bitr4d.2 φ θ ψ
3bitr4d.3 φ τ χ
Assertion 3bitr4rd φ τ θ

Proof

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