![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbie | Unicode version |
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Revised by Wolf Lammen, 30-Apr-2018.) |
Ref | Expression |
---|---|
sbie.1 |
![]() ![]() ![]() ![]() |
sbie.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sbie |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbie.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1519 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sbie.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sbieh 1790 |
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 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-i9 1530 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 |
This theorem is referenced by: sbiev 1792 cbveu 2050 mo4f 2086 bm1.1 2162 eqsb1lem 2280 clelsb1 2282 clelsb2 2283 cbvab 2301 clelsb1f 2323 cbvralf 2697 cbvrexf 2698 cbvreu 2703 sbralie 2723 cbvrab 2737 reu2 2927 rmo4f 2937 nfcdeq 2961 sbcco2 2987 sbcie2g 2998 sbcralt 3041 sbcrext 3042 sbcralg 3043 sbcreug 3045 sbcel12g 3074 sbceqg 3075 cbvralcsf 3121 cbvrexcsf 3122 cbvreucsf 3123 cbvrabcsf 3124 sbss 3533 disjiun 4000 sbcbrg 4059 cbvopab1 4078 cbvmpt 4100 tfis2f 4585 cbviota 5185 relelfvdm 5549 nfvres 5550 cbvriota 5844 bezoutlemnewy 12000 bezoutlemmain 12002 |
Copyright terms: Public domain | W3C validator |