![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm3.14 | Unicode version |
Description: Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 798. The converse holds for decidable propositions, as seen at pm3.13dc 865. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm3.14 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 102 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | con3i 561 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | simpr 103 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | con3i 561 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | jaoi 635 |
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-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm3.1 670 xoranor 1267 difindiss 3185 |
Copyright terms: Public domain | W3C validator |