Metamath Proof Explorer
Description: eqsbc3 with setvar variable on right side of equals sign.
(Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 7-Jul-2021)
|
|
Ref |
Expression |
|
Assertion |
eqsbc3r |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
eqsbc3 |
|
2 |
|
eqcom |
|
3 |
2
|
sbcbii |
|
4 |
|
eqcom |
|
5 |
1 3 4
|
3bitr4g |
|