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 can be refuted for all , then it is not possible to find an for which holds" (and likewise for the converse). Comparing this with dfexdc 1390 illustrates that statements which look similar (to someone used to classical logic) can be different intuitionistically due to different placement of negations. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 1-Feb-2015.) (Revised by Mario Carneiro, 12-May-2015.) |
Ref | Expression |
---|---|
alnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fal 1250 | . . . 4 | |
2 | 1 | pm2.21i 575 | . . 3 |
3 | 2 | 19.23h 1387 | . 2 |
4 | dfnot 1262 | . . 3 | |
5 | 4 | albii 1359 | . 2 |
6 | dfnot 1262 | . 2 | |
7 | 3, 5, 6 | 3bitr4i 201 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wb 98 wal 1241 wfal 1248 wex 1381 |
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 1336 ax-gen 1338 ax-ie2 1383 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-fal 1249 |
This theorem is referenced by: nex 1389 dfexdc 1390 exalim 1391 ax-9 1424 alinexa 1494 nexd 1504 alexdc 1510 19.30dc 1518 19.33b2 1520 alexnim 1539 ax6blem 1540 nf4dc 1560 nf4r 1561 mo2n 1928 disjsn 3432 snprc 3435 dm0rn0 4552 reldm0 4553 dmsn0 4788 dmsn0el 4790 iotanul 4882 imadiflem 4978 imadif 4979 ltexprlemdisj 6704 recexprlemdisj 6728 fzo0 9024 |
Copyright terms: Public domain | W3C validator |