![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xchbinxr | Structured version Visualization version Unicode version |
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
Ref | Expression |
---|---|
xchbinxr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
xchbinxr.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
xchbinxr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xchbinxr.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | xchbinxr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 207 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | xchbinx 316 |
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 190 |
This theorem is referenced by: 3anor 1007 nanbiOLDOLD 1405 2nalexn 1711 2exnaln 1712 sbn 2231 ralnex 2846 rexanali 2852 r2exlem 2922 nss 3502 difdif 3571 difab 3724 sbcnel12g 3786 ssdif0 3835 difin0ss 3845 disjsn 4044 iundif2 4359 iindif2 4361 brsymdif 4473 notzfaus 4592 rexxfr 4634 nssss 4670 reldm0 5071 domtriord 7744 rnelfmlem 21016 dchrfi 24232 wwlknext 25501 df3nandALT2 31107 bj-ssbn 31299 poimirlem1 31986 dvasin 32073 lcvbr3 32634 cvrval2 32885 wopprc 35930 dfss6 36408 |
Copyright terms: Public domain | W3C validator |