![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > xchnxbir | Structured version Unicode version |
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
Ref | Expression |
---|---|
xchnxbir.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
xchnxbir.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
xchnxbir |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xchnxbir.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | xchnxbir.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 202 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | xchnxbi 308 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 185 |
This theorem is referenced by: 3ioran 983 nnelOLD 2791 nsspssun 3667 undif3 3695 ordtri3or 4835 intirr 5300 frxp 6768 ressuppssdif 6796 domunfican 7671 ssfin4 8566 wrdsymb0 12347 symgfix2 16009 gsumdixpOLD 16792 gsumdixp 16793 symgmatr01lem 18561 ppttop 18713 mdegleb 21637 strlem1 25775 isarchi 26319 dfon3 28043 dvtanlem 28565 ftc1anclem3 28593 2exanali 29764 bnj1189 32282 hdmaplem4 35701 mapdh9a 35717 |
Copyright terms: Public domain | W3C validator |