Metamath Proof Explorer
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998)
|
|
Ref |
Expression |
|
Hypotheses |
syl5reqr.1 |
|
|
|
syl5reqr.2 |
|
|
Assertion |
syl5reqr |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
syl5reqr.1 |
|
2 |
|
syl5reqr.2 |
|
3 |
1
|
eqcomi |
|
4 |
3 2
|
syl5req |
|