![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr4g | Unicode version |
Description: More general version of 3bitr4i 201. 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 181 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr4g.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl6bbr 187 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bibi1d 222 pm5.32rd 424 orbi1d 704 dcbid 747 pm4.14dc 786 orbididc 859 3orbi123d 1205 3anbi123d 1206 xorbi2d 1269 xorbi1d 1270 nfbidf 1429 drnf1 1618 drnf2 1619 drsb1 1677 sbal2 1895 eubidh 1903 eubid 1904 mobidh 1931 mobid 1932 eqeq1 2043 eqeq2 2046 eleq1 2097 eleq2 2098 nfceqdf 2174 drnfc1 2191 drnfc2 2192 neeq1 2213 neeq2 2214 neleq1 2295 neleq2 2296 ralbida 2314 rexbida 2315 ralbidv2 2322 rexbidv2 2323 r19.21t 2388 r19.23t 2417 reubida 2485 rmobida 2490 raleqf 2495 rexeqf 2496 reueq1f 2497 rmoeq1f 2498 cbvraldva2 2531 cbvrexdva2 2532 dfsbcq 2760 sbcbid 2810 sbcabel 2833 sbnfc2 2900 psseq1 3025 psseq2 3026 ssconb 3070 uneq1 3084 ineq1 3125 difin2 3193 reuun2 3214 reldisj 3265 undif4 3278 disjssun 3279 sbcssg 3324 eltpg 3407 raltpg 3414 rextpg 3415 opeq1 3540 opeq2 3541 intmin4 3634 dfiun2g 3680 iindif2m 3715 iinin2m 3716 breq 3757 breq1 3758 breq2 3759 treq 3851 opthg2 3967 poeq1 4027 soeq1 4043 ordeq 4075 limeq 4080 rabxfrd 4167 iunpw 4177 opthprc 4334 releq 4365 sbcrel 4369 eqrel 4372 eqrelrel 4384 xpiindim 4416 brcnvg 4459 brresg 4563 resieq 4565 xpcanm 4703 xpcan2m 4704 dmsnopg 4735 dfco2a 4764 cnvpom 4803 cnvsom 4804 iotaeq 4818 sniota 4837 sbcfung 4868 fneq1 4930 fneq2 4931 feq1 4973 feq2 4974 feq3 4975 sbcfng 4987 sbcfg 4988 f1eq1 5030 f1eq2 5031 f1eq3 5032 foeq1 5045 foeq2 5046 foeq3 5047 f1oeq1 5060 f1oeq2 5061 f1oeq3 5062 fun11iun 5090 mpteqb 5204 dffo3 5257 fmptco 5273 dff13 5350 f1imaeq 5357 f1imapss 5358 f1eqcocnv 5374 fliftcnv 5378 isoeq1 5384 isoeq2 5385 isoeq3 5386 isoeq4 5387 isoeq5 5388 isocnv2 5395 acexmid 5454 fnotovb 5490 mpt2eq123 5506 ottposg 5811 dmtpos 5812 smoeq 5846 nnacan 6021 nnmcan 6028 ereq1 6049 ereq2 6050 elecg 6080 ereldm 6085 enfi 6252 creur 7692 eqreznegel 8325 ltxr 8465 icoshftf1o 8629 elfzm11 8723 elfzomelpfzo 8857 nn0ennn 8890 nnesq 9021 cbvrald 9262 bj-dcbi 9383 |
Copyright terms: Public domain | W3C validator |