Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.21 | GIF 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: ¬ wn 3 → wi 4 |
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 2034 exmodc 2056 exmonim 2057 nrexrmo 2673 opthpr 3735 0neqopab 5866 0mnnnnn0 9122 flqeqceilz 10217 |
Copyright terms: Public domain | W3C validator |