![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > iotabidv | Unicode version |
Description: Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.) |
Ref | Expression |
---|---|
iotabidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
iotabidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iotabidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | alrimiv 1884 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | iotabi 5199 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 14 |
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-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-rex 2471 df-uni 3822 df-iota 5190 |
This theorem is referenced by: csbiotag 5221 dffv3g 5523 fveq1 5526 fveq2 5527 fvres 5551 csbfv12g 5564 fvco2 5598 riotaeqdv 5845 riotabidv 5846 riotabidva 5860 ovtposg 6274 shftval 10848 sumeq1 11377 sumeq2 11381 zsumdc 11406 isumclim3 11445 isumshft 11512 prodeq1f 11574 prodeq2w 11578 prodeq2 11579 zproddc 11601 pcval 12310 grpidvalg 12811 grpidpropdg 12812 dfur2g 13214 oppr0g 13329 oppr1g 13330 |
Copyright terms: Public domain | W3C validator |