![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.24 | GIF version |
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm2.24 | ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21 617 | . 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
2 | 1 | com12 30 | 1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in2 615 |
This theorem is referenced by: pm2.24d 622 pm2.53 722 pm2.82 812 pm4.81dc 908 dedlema 969 alexim 1645 eqneqall 2357 elnelall 2454 sotritric 4324 ltxrlt 8022 zltnle 9298 elfzonlteqm1 10209 qltnle 10245 hashfzp1 10803 dfgcd2 12014 oddprmdvds 12351 bj-fast 14463 nnnotnotr 14712 |
Copyright terms: Public domain | W3C validator |