![]() |
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 4325 ltxrlt 8023 zltnle 9299 elfzonlteqm1 10210 qltnle 10246 hashfzp1 10804 dfgcd2 12015 oddprmdvds 12352 bj-fast 14496 nnnotnotr 14745 |
Copyright terms: Public domain | W3C validator |