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 150. 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  395  orc  866  pm2.82  975  dedlema  1045  cases2ALT  1048  eqneqall  2955  elnelall  3063  ralf0  4472  preqsnd  4817  ordnbtwn  6411  suppimacnv  8106  ressuppss  8115  ressuppssdif  8117  infssuni  9288  axpowndlem1  10534  ltlen  11257  znnn0nn  12615  elfzonlteqm1  13649  injresinjlem  13693  addmodlteq  13852  ssnn0fi  13891  hasheqf1oi  14252  hashfzp1  14332  swrdnd2  14544  swrdnd0  14546  swrdccat3blem  14628  repswswrd  14673  dvdsaddre2b  16190  dfgcd2  16428  prm23ge5  16688  oddprmdvds  16776  mdegle0  25445  2lgsoddprm  26767  nb3grprlem1  28331  4cyclusnfrgr  29239  broutsideof2  34710  meran1  34886  bj-andnotim  35056  contrd  36559  pell1qrgaplem  41199  clsk1indlem3  42322  pm2.43cbi  42807  afv2orxorb  45467  requad2  45822  zeo2ALTV  45870  ztprmneprm  46430  line2xlem  46846
  Copyright terms: Public domain W3C validator