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	$$⊢\phi \to \mathrm{Tr}A$$
	trelded.2	$$⊢\psi \to B\in C$$
	trelded.3	$$⊢\chi \to C\in A$$
Assertion	trelded	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to B\in A$$

Proof

Step	Hyp	Ref	Expression
1		trelded.1	$$⊢\phi \to \mathrm{Tr}A$$
2		trelded.2	$$⊢\psi \to B\in C$$
3		trelded.3	$$⊢\chi \to C\in A$$
4		trel	$$⊢\mathrm{Tr}A\to \left(\left(B\in C\wedge C\in A\right)\to B\in A\right)$$
5	4	3impib	$$⊢\left(\mathrm{Tr}A\wedge B\in C\wedge C\in A\right)\to B\in A$$
6	1 2 3 5	syl3an	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to B\in A$$