Theorem sslin 2225

Description: Add left intersection to subclass relation.

Assertion

Ref	Expression
sslin	|- (A (_ B -> (C i^i A) (_ (C i^i B))

Proof of Theorem sslin

Step	Hyp	Ref	Expression
1		ssrin 2224	. 2 |- (A (_ B -> (A i^i C) (_ (B i^i C))
2		incom 2198	. 2 |- (C i^i A) = (A i^i C)
3		incom 2198	. 2 |- (C i^i B) = (B i^i C)
4	1, 2, 3	3sstr4g 2092	1 |- (A (_ B -> (C i^i A) (_ (C i^i B))

Syntax hints:   -> wi 3   i^i cin 2036   (_ wss 2037

This theorem is referenced by:  ss2in 2226  ssres2 3370  ssrnres 3467  sbthlem7 4433  kmlem5 4741  infxpidmlem11 7505  sncld 7726  lpbl 7819  chssoct 9334  cmbr4 9461  5oa 9523  3oalem6 9529  mdslmd4 10168  atcvat4 10232

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-in 2041  df-ss 2043

Copyright terms: Public domain