Theorem bitr3

Description: Closed nested implication form of bitr3i . Derived automatically from bitr3VD . (Contributed by Alan Sare, 31-Dec-2011)

	Ref	Expression
Assertion	bitr3	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜒 ) → ( 𝜓 ↔ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bibi1	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜒 ) ↔ ( 𝜓 ↔ 𝜒 ) ) )
2	1	biimpd	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜒 ) → ( 𝜓 ↔ 𝜒 ) ) )