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 ) |
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 ) |