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  394  orc  864  pm2.82  973  dedlema  1043  cases2ALT  1046  eqneqall  2954  elnelall  3062  ralf0  4444  preqsnd  4789  ordnbtwn  6356  suppimacnv  7990  ressuppss  7999  ressuppssdif  8001  infssuni  9110  axpowndlem1  10353  ltlen  11076  znnn0nn  12433  elfzonlteqm1  13463  injresinjlem  13507  addmodlteq  13666  ssnn0fi  13705  hasheqf1oi  14066  hashfzp1  14146  swrdnd2  14368  swrdnd0  14370  swrdccat3blem  14452  repswswrd  14497  dvdsaddre2b  16016  dfgcd2  16254  prm23ge5  16516  oddprmdvds  16604  mdegle0  25242  2lgsoddprm  26564  nb3grprlem1  27747  4cyclusnfrgr  28656  broutsideof2  34424  meran1  34600  bj-andnotim  34770  contrd  36255  pell1qrgaplem  40695  clsk1indlem3  41653  pm2.43cbi  42138  afv2orxorb  44720  requad2  45075  zeo2ALTV  45123  ztprmneprm  45683  line2xlem  46099