Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993) Allow shortening of eqeq2 . (Revised by Wolf Lammen, 19-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eqeq2d.1 | |- ( ph -> A = B ) |
|
| Assertion | eqeq2d | |- ( ph -> ( C = A <-> C = B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq2d.1 | |- ( ph -> A = B ) |
|
| 2 | 1 | eqeq1d | |- ( ph -> ( A = C <-> B = C ) ) |
| 3 | eqcom | |- ( C = A <-> A = C ) |
|
| 4 | eqcom | |- ( C = B <-> B = C ) |
|
| 5 | 2 3 4 | 3bitr4g | |- ( ph -> ( C = A <-> C = B ) ) |