Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994) Allow shortening of eqcom . (Revised by Wolf Lammen, 19-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eqcomd.1 | |- ( ph -> A = B ) |
|
| Assertion | eqcomd | |- ( ph -> B = A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqcomd.1 | |- ( ph -> A = B ) |
|
| 2 | eqid | |- A = A |
|
| 3 | 1 | eqeq1d | |- ( ph -> ( A = A <-> B = A ) ) |
| 4 | 2 3 | mpbii | |- ( ph -> B = A ) |