![]() |
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 1249 |
. . . 4
![]() ![]() ![]() | |
2 | 1 | pm2.21i 574 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.23h 1384 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | dfnot 1261 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | albii 1356 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | dfnot 1261 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3, 5, 6 | 3bitr4i 201 |
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 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-5 1333 ax-gen 1335 ax-ie2 1380 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-fal 1248 |
This theorem is referenced by: nex 1386 dfexdc 1387 exalim 1388 ax-9 1421 alinexa 1491 nexd 1501 alexdc 1507 19.30dc 1515 19.33b2 1517 alexnim 1536 ax6blem 1537 nf4dc 1557 nf4r 1558 mo2n 1925 disjsn 3423 snprc 3426 dm0rn0 4495 reldm0 4496 dmsn0 4731 dmsn0el 4733 iotanul 4825 imadiflem 4921 imadif 4922 ltexprlemdisj 6580 recexprlemdisj 6602 fzo0 8794 |
Copyright terms: Public domain | W3C validator |