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 545 | 1 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-in2 545 |
This theorem is referenced by: pm2.21d 549 pm2.24 551 pm2.24i 553 pm2.21i 575 pm2.52 582 jarl 584 mtt 610 orel2 645 imorri 668 pm2.42 694 pm2.18dc 750 simplimdc 757 peircedc 820 pm4.82 857 pm5.71dc 868 dedlemb 877 mo2n 1928 exmodc 1950 exmonim 1951 nrexrmo 2526 opthpr 3543 0neqopab 5550 0mnnnnn0 8214 flqeqceilz 9160 |
Copyright terms: Public domain | W3C validator |