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

Theorem pm2.24 103
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.24  |-  ( ph  ->  ( -.  ph  ->  ps ) )

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 102 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
21com12 29 1  |-  ( ph  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm4.81  356  orc  375  pm2.82  826  dedlema  921  prnebg  3943  axpowndlem1  8432  ltlen  9135  injresinjlem  11158  hasheqf1oi  11594  mdegle0  19957  usgra2edg  21359  nb3graprlem1  21417  nbcusgra  21429  wlkdvspthlem  21564  hashnbgravdg  21639  broutsideof2  25964  meran1  26069  pell1qrgaplem  26830  eqneqall  27943  elnelall  27944  swrdnd  28005  4cyclusnfrgra  28127  frgrawopreglem4  28154  pm2.43cbi  28316
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator