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 119
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 144. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.24 (𝜑 → (¬ 𝜑𝜓))

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 118 . 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  379  orc  398  pm2.82  892  dedlema  992  cases2  1004  eqneqall  2792  ordnbtwn  5719  suppimacnv  7170  ressuppss  7178  ressuppssdif  7180  infssuni  8117  axpowndlem1  9275  ltlen  9989  znnn0nn  11321  elfzonlteqm1  12365  injresinjlem  12405  addmodlteq  12562  ssnn0fi  12601  hasheqf1oi  12954  hasheqf1oiOLD  12955  hashfzp1  13030  swrdnd2  13231  swrdccat3blem  13292  repswswrd  13328  dvdsaddre2b  14813  dfgcd2  15047  prm23ge5  15304  oddprmdvds  15391  mdegle0  23558  2lgsoddprm  24858  nb3graprlem1  25746  nbcusgra  25758  wlkdvspthlem  25903  clwwlkprop  26064  hashnbgravdg  26206  4cyclusnfrgra  26312  broutsideof2  31205  meran1  31386  bj-andnotim  31552  contrd  32865  pell1qrgaplem  36251  clsk1indlem3  37157  pm2.43cbi  37541  zeo2ALTV  39918  elnelall  40100  nb3grprlem1  40603  4cyclusnfrgr  41457  ztprmneprm  41913
  Copyright terms: Public domain W3C validator