Theorem trel3

Description: In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994)

	Ref	Expression
Assertion	trel3	|- ( Tr A -> ( ( B e. C /\ C e. D /\ D e. A ) -> B e. A ) )

Proof

Step	Hyp	Ref	Expression
1		3anass	|- ( ( B e. C /\ C e. D /\ D e. A ) <-> ( B e. C /\ ( C e. D /\ D e. A ) ) )
2		trel	|- ( Tr A -> ( ( C e. D /\ D e. A ) -> C e. A ) )
3	2	anim2d	|- ( Tr A -> ( ( B e. C /\ ( C e. D /\ D e. A ) ) -> ( B e. C /\ C e. A ) ) )
4	1 3	syl5bi	|- ( Tr A -> ( ( B e. C /\ C e. D /\ D e. A ) -> ( B e. C /\ C e. A ) ) )
5		trel	|- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )
6	4 5	syld	|- ( Tr A -> ( ( B e. C /\ C e. D /\ D e. A ) -> B e. A ) )