Theorem pm2.24 124

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 153. 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  396  orc  863  pm2.82  972  dedlema  1040  cases2ALT  1043  eqneqall  3027  elnelall  3136  ordnbtwn  6276  suppimacnv  7835  ressuppss  7843  ressuppssdif  7845  infssuni  8809  axpowndlem1  10013  ltlen  10735  znnn0nn  12088  elfzonlteqm1  13107  injresinjlem  13151  addmodlteq  13308  ssnn0fi  13347  hasheqf1oi  13706  hashfzp1  13786  swrdnd2  14011  swrdnd0  14013  swrdccat3blem  14095  repswswrd  14140  dvdsaddre2b  15651  dfgcd2  15888  prm23ge5  16146  oddprmdvds  16233  mdegle0  24665  2lgsoddprm  25986  nb3grprlem1  27156  4cyclusnfrgr  28065  broutsideof2  33578  meran1  33754  bj-andnotim  33917  contrd  35369  pell1qrgaplem  39463  clsk1indlem3  40386  pm2.43cbi  40845  afv2orxorb  43420  requad2  43781  zeo2ALTV  43829  ztprmneprm  44388  line2xlem  44733