![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr3g | Unicode version |
Description: More general version of 3bitr3i 209. 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 193 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitr3g.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrdi 195 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: con2bidc 861 sbal1yz 1978 sbal1 1979 dfsbcq2 2936 iindif2m 3912 opeqex 4204 rabxfrd 4423 eqbrrdv 4676 eqbrrdiv 4677 opelco2g 4747 opelcnvg 4759 ralrnmpt 5602 rexrnmpt 5603 fliftcnv 5736 eusvobj2 5800 f1od2 6172 ottposg 6192 ercnv 6490 exmidpw 6842 djuf1olem 6983 fzen 9923 fihasheq0 10645 divalgb 11789 isprm3 11966 eldvap 12990 |
Copyright terms: Public domain | W3C validator |