![]() |
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 605 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-in2 605 |
This theorem is referenced by: pm2.21d 609 pm2.24 611 pm2.24i 613 pm2.21i 636 jarl 648 mtt 675 orel2 716 imorri 739 pm2.42 767 pm2.18dc 841 simplimdc 846 peircedc 900 pm4.82 935 pm5.71dc 946 dedlemb 955 mo2n 2028 exmodc 2050 exmonim 2051 nrexrmo 2650 opthpr 3707 0neqopab 5824 0mnnnnn0 9033 flqeqceilz 10122 |
Copyright terms: Public domain | W3C validator |