![]() |
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 1371 |
. . . 4
![]() ![]() ![]() | |
2 | 1 | pm2.21i 647 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.23h 1509 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfnot 1382 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | albii 1481 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | dfnot 1382 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3, 5, 6 | 3bitr4i 212 |
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-in1 615 ax-in2 616 ax-5 1458 ax-gen 1460 ax-ie2 1505 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-fal 1370 |
This theorem is referenced by: nex 1511 dfexdc 1512 exalim 1513 ax-9 1542 alinexa 1614 nexd 1624 alexdc 1630 19.30dc 1638 19.33b2 1640 alexnim 1659 nnal 1660 ax6blem 1661 nf4dc 1681 nf4r 1682 mo2n 2066 notm0 3458 disjsn 3669 snprc 3672 dm0rn0 4862 reldm0 4863 dmsn0 5114 dmsn0el 5116 iotanul 5211 imadiflem 5314 imadif 5315 ltexprlemdisj 7635 recexprlemdisj 7659 fzo0 10198 |
Copyright terms: Public domain | W3C validator |