![]() |
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 150. Commuted form of pm2.21 123. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm2.24 | ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21 123 | . 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 395 orc 866 pm2.82 975 dedlema 1045 cases2ALT 1048 eqneqall 2955 elnelall 3063 ralf0 4472 preqsnd 4817 ordnbtwn 6411 suppimacnv 8106 ressuppss 8115 ressuppssdif 8117 infssuni 9288 axpowndlem1 10534 ltlen 11257 znnn0nn 12615 elfzonlteqm1 13649 injresinjlem 13693 addmodlteq 13852 ssnn0fi 13891 hasheqf1oi 14252 hashfzp1 14332 swrdnd2 14544 swrdnd0 14546 swrdccat3blem 14628 repswswrd 14673 dvdsaddre2b 16190 dfgcd2 16428 prm23ge5 16688 oddprmdvds 16776 mdegle0 25445 2lgsoddprm 26767 nb3grprlem1 28331 4cyclusnfrgr 29239 broutsideof2 34710 meran1 34886 bj-andnotim 35056 contrd 36559 pell1qrgaplem 41199 clsk1indlem3 42322 pm2.43cbi 42807 afv2orxorb 45467 requad2 45822 zeo2ALTV 45870 ztprmneprm 46430 line2xlem 46846 |
Copyright terms: Public domain | W3C validator |