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  3914  axpowndlem1  8398  ltlen  9101  injresinjlem  11119  hasheqf1oi  11555  mdegle0  19860  usgra2edg  21261  nbusgra  21299  nb3graprlem1  21319  nbcusgra  21331  wlkdvspthlem  21448  hashnbgravdg  21523  broutsideof2  25763  meran1  25868  pell1qrgaplem  26620  4cyclusnfrgra  27765  frgrawopreglem4  27792  pm2.43cbi  27937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator