This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → Tr ⁡ A
trelded.2 ⊢ ψ → B ∈ C
trelded.3 ⊢ χ → C ∈ A
Assertion trelded ⊢ φ ∧ ψ ∧ χ → B ∈ A

Proof

Step Hyp Ref Expression
1 trelded.1 ⊢ φ → Tr ⁡ A
2 trelded.2 ⊢ ψ → B ∈ C
3 trelded.3 ⊢ χ → C ∈ A
4 trel ⊢ Tr ⁡ A → B ∈ C ∧ C ∈ A → B ∈ A
5 4 3impib ⊢ Tr ⁡ A ∧ B ∈ C ∧ C ∈ A → B ∈ A
6 1 2 3 5 syl3an ⊢ φ ∧ ψ ∧ χ → B ∈ A