Theorem trelded

Description: Deduction form of trel . In a transitive class, the membership relation is transitive. (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	trelded.1	|- ( ph -> Tr A )
	trelded.2	|- ( ps -> B e. C )
	trelded.3	|- ( ch -> C e. A )
Assertion	trelded	|- ( ( ph /\ ps /\ ch ) -> B e. A )

Proof

Step	Hyp	Ref	Expression
1		trelded.1	|- ( ph -> Tr A )
2		trelded.2	|- ( ps -> B e. C )
3		trelded.3	|- ( ch -> C e. A )
4		trel	|- ( Tr A -> ( ( B e. C /\ C e. A ) -> B e. A ) )
5	4	3impib	|- ( ( Tr A /\ B e. C /\ C e. A ) -> B e. A )
6	1 2 3 5	syl3an	|- ( ( ph /\ ps /\ ch ) -> B e. A )