![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xchbinx | Structured version Visualization version Unicode version |
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
Ref | Expression |
---|---|
xchbinx.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
xchbinx.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
xchbinx |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xchbinx.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | xchbinx.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | notbii 298 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitri 253 |
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 189 |
This theorem is referenced by: xchbinxr 313 con1bii 333 pm4.52 494 pm4.54 496 xordi 905 3anor 1000 nancom 1386 nannanOLD 1389 nannot 1391 nanbiOLDOLD 1394 xorneg1 1416 trunanfal 1486 truxortru 1490 truxorfal 1491 falxorfal 1494 nic-mpALT 1554 nic-axALT 1556 sban 2227 sbex 2291 necon3abii 2669 ne3anior 2716 ralnex2 2892 ralnex3 2893 inssdif0 3833 dtruALT 4631 dtruALT2 4643 dm0rn0 5050 brprcneu 5856 0nelfz1 11815 pmltpc 22394 frgrancvvdeqlem2 25752 cvbr2 27929 bnj1143 29595 soseq 30485 brsset 30649 brtxpsd 30654 dffun10 30674 dfint3 30712 brub 30714 wl-nfeqfb 31863 sbcni 32342 lcvbr2 32582 atlrelat1 32881 dfxor5 36353 df3an2 36355 falseral0 38980 nbgrnself 39412 rgrx0ndm 39591 pgrpgt2nabl 40138 lmod1zrnlvec 40274 aacllem 40527 |
Copyright terms: Public domain | W3C validator |