![]() |
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: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 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 442 orbi1d 746 stbid 783 dcbid 792 pm4.14dc 831 orbididc 905 3orbi123d 1257 3anbi123d 1258 xorbi2d 1326 xorbi1d 1327 nfbidf 1487 drnf1 1679 drnf2 1680 drsb1 1738 sbal2 1958 eubidh 1966 eubid 1967 mobidh 1994 mobid 1995 eqeq1 2106 eqeq2 2109 eleq1w 2160 eleq2w 2161 eleq1 2162 eleq2 2163 nfceqdf 2239 drnfc1 2257 drnfc2 2258 neeq1 2280 neeq2 2281 neleq1 2366 neleq2 2367 dfrex2dc 2387 ralbida 2390 rexbida 2391 ralbidv2 2398 rexbidv2 2399 r19.21t 2466 r19.23t 2498 reubida 2570 rmobida 2575 raleqf 2580 rexeqf 2581 reueq1f 2582 rmoeq1f 2583 cbvraldva2 2616 cbvrexdva2 2617 dfsbcq 2864 sbcbi2 2911 sbcbid 2918 eqsbc3r 2921 sbcabel 2942 sbnfc2 3010 ssconb 3156 uneq1 3170 ineq1 3217 difin2 3285 reuun2 3306 reldisj 3361 undif4 3372 disjssun 3373 sbcssg 3419 eltpg 3516 raltpg 3523 rextpg 3524 r19.12sn 3536 opeq1 3652 opeq2 3653 intmin4 3746 dfiun2g 3792 iindif2m 3827 iinin2m 3828 breq 3877 breq1 3878 breq2 3879 treq 3972 opthg2 4099 poeq1 4159 soeq1 4175 frforeq1 4203 freq1 4204 frforeq2 4205 freq2 4206 frforeq3 4207 weeq1 4216 weeq2 4217 ordeq 4232 limeq 4237 rabxfrd 4328 iunpw 4339 opthprc 4528 releq 4559 sbcrel 4563 eqrel 4566 eqrelrel 4578 xpiindim 4614 brcnvg 4658 brresg 4763 resieq 4765 xpcanm 4914 xpcan2m 4915 dmsnopg 4946 dfco2a 4975 cnvpom 5017 cnvsom 5018 iotaeq 5032 sniota 5051 sbcfung 5083 fneq1 5147 fneq2 5148 feq1 5191 feq2 5192 feq3 5193 sbcfng 5206 sbcfg 5207 f1eq1 5259 f1eq2 5260 f1eq3 5261 foeq1 5277 foeq2 5278 foeq3 5279 f1oeq1 5292 f1oeq2 5293 f1oeq3 5294 fun11iun 5322 mpteqb 5443 dffo3 5499 fmptco 5518 dff13 5601 f1imaeq 5608 f1eqcocnv 5624 fliftcnv 5628 isoeq1 5634 isoeq2 5635 isoeq3 5636 isoeq4 5637 isoeq5 5638 isocnv2 5645 acexmid 5705 fnotovb 5746 mpoeq123 5762 ottposg 6082 dmtpos 6083 smoeq 6117 nnacan 6338 nnmcan 6345 ereq1 6366 ereq2 6367 elecg 6397 ereldm 6402 ixpiinm 6548 enfi 6696 creur 8575 eqreznegel 9256 ltxr 9403 icoshftf1o 9615 elfzm11 9712 elfzomelpfzo 9849 nn0ennn 10047 nnesq 10252 rexfiuz 10601 cau4 10728 sumeq2 10967 fisumcom2 11046 dvdsflip 11344 divgcdcoprm0 11575 hashdvds 11689 tpspropd 11985 tgss2 12030 lmbr2 12164 txcnmpt 12223 blininf 12352 blres 12362 xmeterval 12363 xmspropd 12405 mspropd 12406 metequiv 12423 limcdifap 12512 cbvrald 12576 bj-dcbi 12707 |
Copyright terms: Public domain | W3C validator |