This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Deduction form of equcom , symmetry of equality. For the versions for
classes, see eqcom and eqcomd . (Contributed by BJ, 6-Oct-2019)
|
|
Ref |
Expression |
|
Hypothesis |
equcomd.1 |
|- ( ph -> x = y ) |
|
Assertion |
equcomd |
|- ( ph -> y = x ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
equcomd.1 |
|- ( ph -> x = y ) |
| 2 |
|
equcom |
|- ( x = y <-> y = x ) |
| 3 |
1 2
|
sylib |
|- ( ph -> y = x ) |