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 8685 eqreznegel 9374 ltxr 9530 icoshftf1o 9742 elfzm11 9839 elfzomelpfzo 9976 nn0ennn 10174 nnesq 10379 rexfiuz 10729 cau4 10856 sumeq2 11096 fisumcom2 11175 dvdsflip 11476 divgcdcoprm0 11709 hashdvds 11824 tpspropd 12130 tgss2 12175 lmbr2 12310 txcnmpt 12369 txhmeo 12415 blininf 12520 blres 12530 xmeterval 12531 xmspropd 12573 mspropd 12574 metequiv 12591 xmetxpbl 12604 limcdifap 12727 cbvrald 12922 |
Copyright terms: Public domain | W3C validator |