New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Sep-2012.) |
Ref | Expression |
---|---|
pm2.21 | ⊢ (¬ φ → (φ → ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (¬ φ → ¬ φ) | |
2 | 1 | pm2.21d 98 | 1 ⊢ (¬ φ → (φ → ψ)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: pm2.24 101 pm2.18 102 notnot2 104 simplim 143 jarl 155 orel2 372 pm2.42 557 pm4.82 894 pm5.71 902 dedlem0b 919 dedlemb 921 dfnot 1332 cad0 1400 meredith 1404 tbw-bijust 1463 tbw-negdf 1464 ax12dgen2 1726 19.38 1794 nfimdOLD 1809 hbimdOLD 1816 hbimOLD 1818 a16g 1945 sbi2 2064 ax46to6 2164 ax467to6 2171 ax467to7 2172 ax11indi 2196 mo 2226 mo2 2233 exmo 2249 2mo 2282 nrexrmo 2828 elab3gf 2990 moeq3 3013 pwadjoin 4119 dff3 5420 |
Copyright terms: Public domain | W3C validator |