![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.21 | Unicode version |
Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by Mario Carneiro, 12-May-2015.) |
Ref | Expression |
---|---|
pm2.21 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-in2 578 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-in2 578 |
This theorem is referenced by: pm2.21d 582 pm2.24 584 pm2.24i 586 pm2.21i 608 pm2.52 615 jarl 617 mtt 643 orel2 678 imorri 701 pm2.42 727 pm2.18dc 784 simplimdc 791 peircedc 854 pm4.82 892 pm5.71dc 903 dedlemb 912 mo2n 1971 exmodc 1993 exmonim 1994 nrexrmo 2575 opthpr 3584 0neqopab 5602 0mnnnnn0 8457 flqeqceilz 9470 |
Copyright terms: Public domain | W3C validator |