![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr4g | Unicode version |
Description: More general version of 3bitr4i 212. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3bitr4g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4g.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr4g.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr4g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4g.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr4g.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitrid 192 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr4g.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitr4di 198 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bibi1d 233 pm5.32rd 451 orbi1d 792 stbid 833 dcbid 839 pm4.14dc 891 orbididc 955 3orbi123d 1322 3anbi123d 1323 xorbi2d 1391 xorbi1d 1392 nfbidf 1550 drnf1 1744 drnf2 1745 drsb1 1810 sbal2 2032 eubidh 2044 eubid 2045 mobidh 2072 mobid 2073 eqeq1 2196 eqeq2 2199 eleq1w 2250 eleq2w 2251 eleq1 2252 eleq2 2253 cbvabw 2312 eqabdv 2318 nfceqdf 2331 drnfc1 2349 drnfc2 2350 neeq1 2373 neeq2 2374 neleq1 2459 neleq2 2460 dfrex2dc 2481 ralbida 2484 rexbida 2485 ralbidv2 2492 rexbidv2 2493 ralbid2 2494 rexbid2 2495 r19.21t 2565 r19.23t 2597 reubida 2672 rmobida 2677 raleqf 2682 rexeqf 2683 reueq1f 2684 rmoeq1f 2685 cbvraldva2 2725 cbvrexdva2 2726 dfsbcq 2979 sbceqbid 2984 sbcbi2 3028 sbcbid 3035 eqsbc2 3038 sbcabel 3059 sbnfc2 3132 ssconb 3283 uneq1 3297 ineq1 3344 difin2 3412 reuun2 3433 reldisj 3489 undif4 3500 disjssun 3501 sbcssg 3547 eltpg 3652 raltpg 3660 rextpg 3661 r19.12sn 3673 opeq1 3793 opeq2 3794 intmin4 3887 dfiun2g 3933 iindif2m 3969 iinin2m 3970 breq 4020 breq1 4021 breq2 4022 treq 4122 opthg2 4257 poeq1 4317 soeq1 4333 frforeq1 4361 freq1 4362 frforeq2 4363 freq2 4364 frforeq3 4365 weeq1 4374 weeq2 4375 ordeq 4390 limeq 4395 rabxfrd 4487 iunpw 4498 opthprc 4695 releq 4726 sbcrel 4730 eqrel 4733 eqrelrel 4745 xpiindim 4782 brcnvg 4826 brresg 4933 resieq 4935 xpcanm 5086 xpcan2m 5087 dmsnopg 5118 dfco2a 5147 cnvpom 5189 cnvsom 5190 iotaeq 5204 sniota 5226 sbcfung 5259 fneq1 5323 fneq2 5324 feq1 5367 feq2 5368 feq3 5369 sbcfng 5382 sbcfg 5383 f1eq1 5435 f1eq2 5436 f1eq3 5437 foeq1 5453 foeq2 5454 foeq3 5455 f1oeq1 5468 f1oeq2 5469 f1oeq3 5470 fun11iun 5501 mpteqb 5627 dffo3 5684 fmptco 5703 dff13 5790 f1imaeq 5797 f1eqcocnv 5813 fliftcnv 5817 isoeq1 5823 isoeq2 5824 isoeq3 5825 isoeq4 5826 isoeq5 5827 isocnv2 5834 acexmid 5895 fnotovb 5939 mpoeq123 5955 ottposg 6280 dmtpos 6281 smoeq 6315 nnacan 6537 nnmcan 6544 ereq1 6566 ereq2 6567 elecg 6599 ereldm 6604 ixpiinm 6750 enfi 6901 elfi2 7001 fipwssg 7008 ctssdccl 7140 tapeq1 7281 tapeq2 7282 creur 8946 eqreznegel 9644 ltxr 9805 icoshftf1o 10021 elfzm11 10121 elfzomelpfzo 10261 nn0ennn 10464 nnesq 10671 rexfiuz 11030 cau4 11157 sumeq2 11399 fisumcom2 11478 fprodcom2fi 11666 dvdsflip 11889 divgcdcoprm0 12133 hashdvds 12253 4sqlem12 12434 imasaddfnlemg 12791 issgrpv 12867 issgrpn0 12868 mndpropd 12901 ismhm 12913 mhmpropd 12918 issubm2 12925 grppropd 12962 grpinvcnv 13012 conjghm 13215 conjnmzb 13219 ghmpropd 13222 cmnpropd 13234 ablpropd 13235 eqgabl 13267 rngpropd 13309 issrg 13319 ringpropd 13392 crngpropd 13393 subrngpropd 13563 subrgpropd 13595 lmodprop2d 13664 islssm 13673 islssmg 13674 lsspropdg 13747 df2idl2rng 13823 tpspropd 13996 tgss2 14039 lmbr2 14174 txcnmpt 14233 txhmeo 14279 blininf 14384 blres 14394 xmeterval 14395 xmspropd 14437 mspropd 14438 metequiv 14455 xmetxpbl 14468 limcdifap 14591 cbvrald 15001 bj-indeq 15142 |
Copyright terms: Public domain | W3C validator |