Metamath Proof Explorer


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 )