Metamath Proof Explorer

Theorem trel3

Description: In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994)

Ref Expression
Assertion trel3 ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ D ∧ D ∈ A → B ∈ A

Proof

Step Hyp Ref Expression
1 3anass ⊢ B ∈ C ∧ C ∈ D ∧ D ∈ A ↔ B ∈ C ∧ C ∈ D ∧ D ∈ A
2 trel ⊢ Tr ⁡ A → C ∈ D ∧ D ∈ A → C ∈ A
3 2 anim2d ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ D ∧ D ∈ A → B ∈ C ∧ C ∈ A
4 1 3 syl5bi ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ D ∧ D ∈ A → B ∈ C ∧ C ∈ A
5 trel ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ A → B ∈ A
6 4 5 syld ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ D ∧ D ∈ A → B ∈ A