![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alnex | Unicode version |
Description: Theorem 19.7 of [Margaris] p. 89. To read this
intuitionistically, think
of it as "if ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
alnex |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fal 1292 |
. . . 4
![]() ![]() ![]() | |
2 | 1 | pm2.21i 608 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.23h 1428 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfnot 1303 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | albii 1400 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | dfnot 1303 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3, 5, 6 | 3bitr4i 210 |
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 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-5 1377 ax-gen 1379 ax-ie2 1424 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-fal 1291 |
This theorem is referenced by: nex 1430 dfexdc 1431 exalim 1432 ax-9 1465 alinexa 1535 nexd 1545 alexdc 1551 19.30dc 1559 19.33b2 1561 alexnim 1580 ax6blem 1581 nf4dc 1601 nf4r 1602 mo2n 1971 disjsn 3472 snprc 3475 dm0rn0 4600 reldm0 4601 dmsn0 4838 dmsn0el 4840 iotanul 4932 imadiflem 5029 imadif 5030 ltexprlemdisj 6928 recexprlemdisj 6952 fzo0 9324 |
Copyright terms: Public domain | W3C validator |