![]() |
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 1360 |
. . . 4
![]() ![]() ![]() | |
2 | 1 | pm2.21i 646 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.23h 1498 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfnot 1371 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | albii 1470 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | dfnot 1371 |
. 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 614 ax-in2 615 ax-5 1447 ax-gen 1449 ax-ie2 1494 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-fal 1359 |
This theorem is referenced by: nex 1500 dfexdc 1501 exalim 1502 ax-9 1531 alinexa 1603 nexd 1613 alexdc 1619 19.30dc 1627 19.33b2 1629 alexnim 1648 nnal 1649 ax6blem 1650 nf4dc 1670 nf4r 1671 mo2n 2054 notm0 3443 disjsn 3654 snprc 3657 dm0rn0 4844 reldm0 4845 dmsn0 5096 dmsn0el 5098 iotanul 5193 imadiflem 5295 imadif 5296 ltexprlemdisj 7604 recexprlemdisj 7628 fzo0 10167 |
Copyright terms: Public domain | W3C validator |