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	⊢ ( 𝜑 → Tr 𝐴 )
	trelded.2	⊢ ( 𝜓 → 𝐵 ∈ 𝐶 )
	trelded.3	⊢ ( 𝜒 → 𝐶 ∈ 𝐴 )
Assertion	trelded	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		trelded.1	⊢ ( 𝜑 → Tr 𝐴 )
2		trelded.2	⊢ ( 𝜓 → 𝐵 ∈ 𝐶 )
3		trelded.3	⊢ ( 𝜒 → 𝐶 ∈ 𝐴 )
4		trel	⊢ ( Tr 𝐴 → ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )
5	4	3impib	⊢ ( ( Tr 𝐴 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
6	1 2 3 5	syl3an	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝐵 ∈ 𝐴 )