Metamath Proof Explorer


Theorem trin

Description: The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994)

Ref Expression
Assertion trin TrATrBTrAB

Proof

Step Hyp Ref Expression
1 elin xABxAxB
2 trss TrAxAxA
3 trss TrBxBxB
4 2 3 im2anan9 TrATrBxAxBxAxB
5 1 4 syl5bi TrATrBxABxAxB
6 ssin xAxBxAB
7 5 6 syl6ib TrATrBxABxAB
8 7 ralrimiv TrATrBxABxAB
9 dftr3 TrABxABxAB
10 8 9 sylibr TrATrBTrAB