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 447 orbi1d 781 stbid 818 dcbid 824 pm4.14dc 876 orbididc 938 3orbi123d 1290 3anbi123d 1291 xorbi2d 1359 xorbi1d 1360 nfbidf 1520 drnf1 1712 drnf2 1713 drsb1 1772 sbal2 1998 eubidh 2006 eubid 2007 mobidh 2034 mobid 2035 eqeq1 2147 eqeq2 2150 eleq1w 2201 eleq2w 2202 eleq1 2203 eleq2 2204 nfceqdf 2281 drnfc1 2299 drnfc2 2300 neeq1 2322 neeq2 2323 neleq1 2408 neleq2 2409 dfrex2dc 2429 ralbida 2432 rexbida 2433 ralbidv2 2440 rexbidv2 2441 ralbid2 2442 rexbid2 2443 r19.21t 2510 r19.23t 2542 reubida 2615 rmobida 2620 raleqf 2625 rexeqf 2626 reueq1f 2627 rmoeq1f 2628 cbvraldva2 2664 cbvrexdva2 2665 dfsbcq 2915 sbcbi2 2963 sbcbid 2970 eqsbc3r 2973 sbcabel 2994 sbnfc2 3065 ssconb 3214 uneq1 3228 ineq1 3275 difin2 3343 reuun2 3364 reldisj 3419 undif4 3430 disjssun 3431 sbcssg 3477 eltpg 3576 raltpg 3584 rextpg 3585 r19.12sn 3597 opeq1 3713 opeq2 3714 intmin4 3807 dfiun2g 3853 iindif2m 3888 iinin2m 3889 breq 3939 breq1 3940 breq2 3941 treq 4040 opthg2 4169 poeq1 4229 soeq1 4245 frforeq1 4273 freq1 4274 frforeq2 4275 freq2 4276 frforeq3 4277 weeq1 4286 weeq2 4287 ordeq 4302 limeq 4307 rabxfrd 4398 iunpw 4409 opthprc 4598 releq 4629 sbcrel 4633 eqrel 4636 eqrelrel 4648 xpiindim 4684 brcnvg 4728 brresg 4835 resieq 4837 xpcanm 4986 xpcan2m 4987 dmsnopg 5018 dfco2a 5047 cnvpom 5089 cnvsom 5090 iotaeq 5104 sniota 5123 sbcfung 5155 fneq1 5219 fneq2 5220 feq1 5263 feq2 5264 feq3 5265 sbcfng 5278 sbcfg 5279 f1eq1 5331 f1eq2 5332 f1eq3 5333 foeq1 5349 foeq2 5350 foeq3 5351 f1oeq1 5364 f1oeq2 5365 f1oeq3 5366 fun11iun 5396 mpteqb 5519 dffo3 5575 fmptco 5594 dff13 5677 f1imaeq 5684 f1eqcocnv 5700 fliftcnv 5704 isoeq1 5710 isoeq2 5711 isoeq3 5712 isoeq4 5713 isoeq5 5714 isocnv2 5721 acexmid 5781 fnotovb 5822 mpoeq123 5838 ottposg 6160 dmtpos 6161 smoeq 6195 nnacan 6416 nnmcan 6423 ereq1 6444 ereq2 6445 elecg 6475 ereldm 6480 ixpiinm 6626 enfi 6775 elfi2 6868 fipwssg 6875 ctssdccl 7004 creur 8741 eqreznegel 9433 ltxr 9592 icoshftf1o 9804 elfzm11 9902 elfzomelpfzo 10039 nn0ennn 10237 nnesq 10442 rexfiuz 10793 cau4 10920 sumeq2 11160 fisumcom2 11239 dvdsflip 11585 divgcdcoprm0 11818 hashdvds 11933 tpspropd 12242 tgss2 12287 lmbr2 12422 txcnmpt 12481 txhmeo 12527 blininf 12632 blres 12642 xmeterval 12643 xmspropd 12685 mspropd 12686 metequiv 12703 xmetxpbl 12716 limcdifap 12839 cbvrald 13166 |
Copyright terms: Public domain | W3C validator |