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 604 | 1 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-in2 604 |
This theorem is referenced by: pm2.21d 608 pm2.24 610 pm2.24i 612 pm2.21i 635 jarl 647 mtt 674 orel2 715 imorri 738 pm2.42 766 pm2.18dc 840 simplimdc 845 peircedc 899 pm4.82 934 pm5.71dc 945 dedlemb 954 mo2n 2025 exmodc 2047 exmonim 2048 nrexrmo 2645 opthpr 3694 0neqopab 5809 0mnnnnn0 9002 flqeqceilz 10084 |
Copyright terms: Public domain | W3C validator |