MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.24 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm2.21 123 . 2 𝜑 → (𝜑𝜓))
21com12 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  394  orc  863  pm2.82  971  dedlema  1039  cases2ALT  1042  eqneqall  3032  elnelall  3141  ordnbtwn  6280  suppimacnv  7837  ressuppss  7845  ressuppssdif  7847  infssuni  8809  axpowndlem1  10013  ltlen  10735  znnn0nn  12088  elfzonlteqm1  13108  injresinjlem  13152  addmodlteq  13309  ssnn0fi  13348  hasheqf1oi  13707  hashfzp1  13787  swrdnd2  14012  swrdnd0  14014  swrdccat3blem  14096  repswswrd  14141  dvdsaddre2b  15652  dfgcd2  15889  prm23ge5  16147  oddprmdvds  16234  mdegle0  24605  2lgsoddprm  25925  nb3grprlem1  27095  4cyclusnfrgr  28004  broutsideof2  33486  meran1  33662  bj-andnotim  33825  contrd  35262  pell1qrgaplem  39354  clsk1indlem3  40277  pm2.43cbi  40736  afv2orxorb  43312  requad2  43639  zeo2ALTV  43687  ztprmneprm  44297  line2xlem  44642
  Copyright terms: Public domain W3C validator