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

Theorem pm2.24 104
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 103 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
21com12 30 1  |-  ( ph  ->  ( -.  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm4.81  357  orc  376  pm2.82  827  dedlema  922  prnebg  3981  infssuni  7399  axpowndlem1  8474  ltlen  9177  injresinjlem  11201  hasheqf1oi  11637  mdegle0  20002  usgra2edg  21404  nb3graprlem1  21462  nbcusgra  21474  wlkdvspthlem  21609  hashnbgravdg  21684  broutsideof2  26058  meran1  26163  pell1qrgaplem  26938  eqneqall  28052  elnelall  28053  swrdnd  28204  swrdvalodm2  28210  swrdvalodm  28211  swrdccat3blem  28240  4cyclusnfrgra  28471  frgrawopreglem4  28498  pm2.43cbi  28663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator