Theorem pm2.24 109

Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)

Assertion

Ref	Expression
pm2.24

Proof of Theorem pm2.24

Step	Hyp	Ref	Expression
1		pm2.21 108	. 2
2	1	com12 31	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  pm4.81  366  orc  385  pm2.82  852  dedlema  954  cases2  971  ifptru  1388  eqneqall  2664  suppimacnv  6929  ressuppss  6938  ressuppssdif  6940  infssuni  7831  axpowndlem1  8993  ltlen  9707  elfzonlteqm1  11891  injresinjlem  11925  ssnn0fi  12094  hasheqf1oi  12424  swrdnd  12657  swrdvalodm2  12664  swrdvalodm  12665  swrdccat3blem  12720  repswswrd  12756  mdegle0  22477  nb3graprlem1  24451  nbcusgra  24463  wlkdvspthlem  24609  clwwlkprop  24770  hashnbgravdg  24913  4cyclusnfrgra  25019  broutsideof2  29772  meran1  29876  contrd  30497  pell1qrgaplem  30809  znnn0nn  31489  elnelall  32293  ztprmneprm  32936  pm2.43cbi  33288  bj-andnotim  34177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8