![]() |
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 3445 disjsn 3656 snprc 3659 dm0rn0 4846 reldm0 4847 dmsn0 5098 dmsn0el 5100 iotanul 5195 imadiflem 5297 imadif 5298 ltexprlemdisj 7607 recexprlemdisj 7631 fzo0 10170 |
Copyright terms: Public domain | W3C validator |