Description: A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eqvreltrd.1 | |- ( ph -> EqvRel R ) |
|
eqvreltrd.2 | |- ( ph -> A R B ) |
||
eqvreltrd.3 | |- ( ph -> B R C ) |
||
Assertion | eqvreltrd | |- ( ph -> A R C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqvreltrd.1 | |- ( ph -> EqvRel R ) |
|
2 | eqvreltrd.2 | |- ( ph -> A R B ) |
|
3 | eqvreltrd.3 | |- ( ph -> B R C ) |
|
4 | 1 | eqvreltr | |- ( ph -> ( ( A R B /\ B R C ) -> A R C ) ) |
5 | 2 3 4 | mp2and | |- ( ph -> A R C ) |