Theorem pm2.24 125

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 151. Commuted form of pm2.21 124. (Contributed by NM, 3-Jan-2005.)

Assertion

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

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 124	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2	1	com12 33	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  398  orc  880  pm2.82  991  dedlema  1061  cases2ALT  1064  eqneqall  2969  pm2.24nel  3077  preqsnd  4825  ordnbtwn  6458  suppimacnv  8171  ressuppss  8180  ressuppssdif  8182  infssuni  9304  axpowndlem1  10583  ltlen  11312  znnn0nn  12708  elfzonlteqm1  13772  injresinjlem  13821  addmodlteq  13984  ssnn0fi  14023  hasheqf1oi  14389  hashfzp1  14470  swrdnd2  14695  swrdnd0  14697  swrdccat3blem  14778  repswswrd  14823  dvdsaddre2b  16366  dfgcd2  16605  prm23ge5  16876  oddprmdvds  16964  isfieldidl  21367  mdegle0  26215  2lgsoddprm  27558  nb3grprlem1  29708  4cyclusnfrgr  30621  broutsideof2  36592  meran1  36900  bj-andnotim  37159  contrd  38724  pell1qrgaplem  43580  clsk1indlem3  44749  pm2.43cbi  45207  afv2orxorb  47942  requad2  48365  zeo2ALTV  48413  ztprmneprm  49104  line2xlem  49510