Metamath Proof Explorer


Theorem eqvreltr4d

Description: A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

Ref Expression
Hypotheses eqvreltr4d.1
|- ( ph -> EqvRel R )
eqvreltr4d.2
|- ( ph -> A R B )
eqvreltr4d.3
|- ( ph -> C R B )
Assertion eqvreltr4d
|- ( ph -> A R C )

Proof

Step Hyp Ref Expression
1 eqvreltr4d.1
 |-  ( ph -> EqvRel R )
2 eqvreltr4d.2
 |-  ( ph -> A R B )
3 eqvreltr4d.3
 |-  ( ph -> C R B )
4 1 3 eqvrelsym
 |-  ( ph -> B R C )
5 1 2 4 eqvreltrd
 |-  ( ph -> A R C )