| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: A useful inference for substituting definitions into an equality. |
| Ref | Expression |
|---|---|
| eqeqan12rd.1 |
|
| eqeqan12rd.2 |
|
| Ref | Expression |
|---|---|
| eqeqan12rd |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeqan12rd.1 |
. . 3
| |
| 2 | eqeqan12rd.2 |
. . 3
| |
| 3 | 1, 2 | eqeqan12d 2156 |
. 2
|
| 4 | 3 | ancoms 416 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: fvopab4gf 4830 fvopabgf 4836 fvopabnf 4837 tfrlem5 5287 inf3lema 5947 aceq8a 6199 numth 6356 zorn2 6369 mulgcdlem2 9352 fsumcnlem 10133 effoi 10970 eigorthi 12232 prtoptop 15684 bfplem3 16824 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 1593 ax-17 1605 ax-4 1608 ax-5o 1610 ax-ext 2123 |
| This theorem depends on definitions: df-bi 220 df-an 339 df-cleq 2134 |