Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2.24 | Structured version Visualization version GIF version |
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 145. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm2.24 | ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21 119 | . 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | |
2 | 1 | com12 32 | 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: pm4.81 380 orc 399 pm2.82 893 dedlema 993 cases2 1005 eqneqall 2793 ordnbtwn 5733 suppimacnv 7193 ressuppss 7201 ressuppssdif 7203 infssuni 8140 axpowndlem1 9298 ltlen 10017 znnn0nn 11365 elfzonlteqm1 12410 injresinjlem 12450 addmodlteq 12607 ssnn0fi 12646 hasheqf1oi 13002 hasheqf1oiOLD 13003 hashfzp1 13078 swrdnd2 13285 swrdccat3blem 13346 repswswrd 13382 dvdsaddre2b 14867 dfgcd2 15101 prm23ge5 15358 oddprmdvds 15445 mdegle0 23641 2lgsoddprm 24941 nb3graprlem1 25980 nbcusgra 25992 wlkdvspthlem 26137 clwwlkprop 26298 hashnbgravdg 26440 4cyclusnfrgra 26546 broutsideof2 31399 meran1 31580 bj-andnotim 31746 contrd 33069 pell1qrgaplem 36455 clsk1indlem3 37361 pm2.43cbi 37745 zeo2ALTV 40120 elnelall 40302 nb3grprlem1 40608 4cyclusnfrgr 41462 ztprmneprm 41918 |
Copyright terms: Public domain | W3C validator |