Theorem pm2.24 124

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.)

Assertion

Ref	Expression
pm2.24	⊢ (𝜑 → (¬ 𝜑 → 𝜓))

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 123	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (𝜑 → (¬ 𝜑 → 𝜓))

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  393  orc  868  pm2.82  978  dedlema  1046  cases2ALT  1049  eqneqall  2943  pm2.24nel  3049  preqsnd  4802  ordnbtwn  6418  suppimacnv  8124  ressuppss  8133  ressuppssdif  8135  infssuni  9256  axpowndlem1  10520  ltlen  11247  znnn0nn  12640  elfzonlteqm1  13696  injresinjlem  13745  addmodlteq  13908  ssnn0fi  13947  hasheqf1oi  14313  hashfzp1  14393  swrdnd2  14618  swrdnd0  14620  swrdccat3blem  14701  repswswrd  14746  dvdsaddre2b  16276  dfgcd2  16515  prm23ge5  16786  oddprmdvds  16874  mdegle0  26042  2lgsoddprm  27379  nb3grprlem1  29449  4cyclusnfrgr  30362  broutsideof2  36304  meran1  36593  bj-andnotim  36853  contrd  38418  pell1qrgaplem  43301  clsk1indlem3  44470  pm2.43cbi  44945  afv2orxorb  47676  requad2  48099  zeo2ALTV  48147  ztprmneprm  48823  line2xlem  49229