![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > csbconstg | Unicode version |
Description: Substitution doesn't
affect a constant ![]() ![]() |
Ref | Expression |
---|---|
csbconstg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2235 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | csbconstgf 2958 |
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 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-sbc 2855 df-csb 2948 |
This theorem is referenced by: sbcel1g 2964 sbceq1g 2965 sbcel2g 2966 sbceq2g 2967 csbidmg 2998 sbcbr12g 3917 sbcbr1g 3918 sbcbr2g 3919 sbcrel 4553 csbcnvg 4651 csbresg 4748 sbcfung 5073 csbfv12g 5375 csbfv2g 5376 elfvmptrab 5434 csbov12g 5726 csbov1g 5727 csbov2g 5728 |
Copyright terms: Public domain | W3C validator |