Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr4g | Unicode version |
Description: More general version of 3bitr4i 211. 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 | syl5bb 191 | . 2 |
4 | 3bitr4g.3 | . 2 | |
5 | 3, 4 | syl6bbr 197 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: bibi1d 232 pm5.32rd 446 orbi1d 765 stbid 802 dcbid 808 pm4.14dc 860 orbididc 922 3orbi123d 1274 3anbi123d 1275 xorbi2d 1343 xorbi1d 1344 nfbidf 1504 drnf1 1696 drnf2 1697 drsb1 1755 sbal2 1975 eubidh 1983 eubid 1984 mobidh 2011 mobid 2012 eqeq1 2124 eqeq2 2127 eleq1w 2178 eleq2w 2179 eleq1 2180 eleq2 2181 nfceqdf 2257 drnfc1 2275 drnfc2 2276 neeq1 2298 neeq2 2299 neleq1 2384 neleq2 2385 dfrex2dc 2405 ralbida 2408 rexbida 2409 ralbidv2 2416 rexbidv2 2417 r19.21t 2484 r19.23t 2516 reubida 2589 rmobida 2594 raleqf 2599 rexeqf 2600 reueq1f 2601 rmoeq1f 2602 cbvraldva2 2635 cbvrexdva2 2636 dfsbcq 2884 sbcbi2 2931 sbcbid 2938 eqsbc3r 2941 sbcabel 2962 sbnfc2 3030 ssconb 3179 uneq1 3193 ineq1 3240 difin2 3308 reuun2 3329 reldisj 3384 undif4 3395 disjssun 3396 sbcssg 3442 eltpg 3539 raltpg 3546 rextpg 3547 r19.12sn 3559 opeq1 3675 opeq2 3676 intmin4 3769 dfiun2g 3815 iindif2m 3850 iinin2m 3851 breq 3901 breq1 3902 breq2 3903 treq 4002 opthg2 4131 poeq1 4191 soeq1 4207 frforeq1 4235 freq1 4236 frforeq2 4237 freq2 4238 frforeq3 4239 weeq1 4248 weeq2 4249 ordeq 4264 limeq 4269 rabxfrd 4360 iunpw 4371 opthprc 4560 releq 4591 sbcrel 4595 eqrel 4598 eqrelrel 4610 xpiindim 4646 brcnvg 4690 brresg 4797 resieq 4799 xpcanm 4948 xpcan2m 4949 dmsnopg 4980 dfco2a 5009 cnvpom 5051 cnvsom 5052 iotaeq 5066 sniota 5085 sbcfung 5117 fneq1 5181 fneq2 5182 feq1 5225 feq2 5226 feq3 5227 sbcfng 5240 sbcfg 5241 f1eq1 5293 f1eq2 5294 f1eq3 5295 foeq1 5311 foeq2 5312 foeq3 5313 f1oeq1 5326 f1oeq2 5327 f1oeq3 5328 fun11iun 5356 mpteqb 5479 dffo3 5535 fmptco 5554 dff13 5637 f1imaeq 5644 f1eqcocnv 5660 fliftcnv 5664 isoeq1 5670 isoeq2 5671 isoeq3 5672 isoeq4 5673 isoeq5 5674 isocnv2 5681 acexmid 5741 fnotovb 5782 mpoeq123 5798 ottposg 6120 dmtpos 6121 smoeq 6155 nnacan 6376 nnmcan 6383 ereq1 6404 ereq2 6405 elecg 6435 ereldm 6440 ixpiinm 6586 enfi 6735 elfi2 6828 fipwssg 6835 ctssdccl 6964 creur 8681 eqreznegel 9362 ltxr 9517 icoshftf1o 9729 elfzm11 9826 elfzomelpfzo 9963 nn0ennn 10161 nnesq 10366 rexfiuz 10716 cau4 10843 sumeq2 11083 fisumcom2 11162 dvdsflip 11461 divgcdcoprm0 11694 hashdvds 11808 tpspropd 12114 tgss2 12159 lmbr2 12294 txcnmpt 12353 txhmeo 12399 blininf 12504 blres 12514 xmeterval 12515 xmspropd 12557 mspropd 12558 metequiv 12575 xmetxpbl 12588 limcdifap 12711 cbvrald 12891 |
Copyright terms: Public domain | W3C validator |