This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Alan Sare Conventional Metamath proofs, some derived from VD proofs 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 𝐴 )
trelded.2 ⊢ ( 𝜓 → 𝐵 ∈ 𝐶 )
trelded.3 ⊢ ( 𝜒 → 𝐶 ∈ 𝐴 )
Assertion
trelded ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝐵 ∈ 𝐴 )
Proof
Step
Hyp
Ref
Expression
1
trelded.1 ⊢ ( 𝜑 → Tr 𝐴 )
2
trelded.2 ⊢ ( 𝜓 → 𝐵 ∈ 𝐶 )
3
trelded.3 ⊢ ( 𝜒 → 𝐶 ∈ 𝐴 )
4
trel ⊢ ( Tr 𝐴 → ( ( 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 ) )
5
4
3impib ⊢ ( ( Tr 𝐴 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
6
1 2 3 5
syl3an ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝐵 ∈ 𝐴 )