![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr3g | Unicode version |
Description: More general version of 3bitr3i 210. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |
Ref | Expression |
---|---|
3bitr3g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3g.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
3bitr3g.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3bitr3g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3g.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3bitr3g.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr3id 194 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3g.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrdi 196 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: con2bidc 876 sbal1yz 2013 sbal1 2014 dfsbcq2 2980 iindif2m 3969 opeqex 4267 rabxfrd 4487 eqbrrdv 4741 eqbrrdiv 4742 opelco2g 4813 opelcnvg 4825 ralrnmpt 5679 rexrnmpt 5680 fliftcnv 5817 eusvobj2 5883 f1od2 6261 ottposg 6281 ercnv 6581 exmidpw 6937 djuf1olem 7083 fzen 10075 fihasheq0 10808 divalgb 11965 isprm3 12153 eldvap 14628 |
Copyright terms: Public domain | W3C validator |