![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3bitr3g | Structured version Visualization version Unicode version |
Description: More general version of 3bitr3i 283. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |
Ref | Expression |
---|---|
3bitr3g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3g.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3g.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr3g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3g.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr3g.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5bbr 267 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3g.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl6bb 269 |
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: notbid 300 cador 1521 equequ2 1878 dfsbcq2 3281 unineq 3704 iindif2 4360 reusv2 4622 rabxfrd 4634 opeqex 4705 eqbrrdv 4950 eqbrrdiv 4951 opelco2g 5020 opelcnvg 5032 ralrnmpt 6053 fliftcnv 6228 eusvobj2 6307 ottpos 7008 smoiso 7106 ercnv 7409 ordiso2 8055 cantnfrescl 8206 cantnfp1lem3 8210 cantnflem1b 8216 cantnflem1 8219 cnfcom 8230 cnfcom3lem 8233 carden2 8446 cardeq0 9002 axpownd 9051 fpwwe2lem9 9088 fzen 11844 hasheq0 12575 incexc2 13944 divalglem4 14423 divalglem8 14428 divalgb 14433 divalgmod 14435 sadadd 14489 sadass 14493 smuval2 14504 smumul 14515 isprm3 14681 vdwmc 14976 imasleval 15495 acsfn2 15617 invsym2 15716 yoniso 16218 pmtrfmvdn0 17151 dprd2d2 17725 cmpfi 20471 xkoinjcn 20750 tgpconcomp 21175 iscau3 22296 mbfimaopnlem 22659 ellimc3 22882 eldv 22901 eltayl 23363 atandm3 23852 el2wlkonot 25645 el2spthonot 25646 rmoxfrdOLD 28176 rmoxfrd 28177 opeldifid 28258 2ndpreima 28336 f1od2 28357 ordtconlem1 28778 bnj1253 29874 wl-dral1d 31908 wl-sb8et 31925 wl-equsb3 31928 wl-sb8eut 31950 wl-ax11-lem8 31966 poimirlem2 31986 poimirlem16 32000 poimirlem18 32002 poimirlem21 32005 poimirlem22 32006 eqbrrdv2 32479 islpln5 33144 islvol5 33188 radcnvrat 36706 trsbc 36944 aacllem 40812 |
Copyright terms: Public domain | W3C validator |