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 ( 𝜑 → ( 𝜏𝜓 ) )