Theorem syl5sseqr 3654

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
syl5sseqr.1	|- B C_ A
syl5sseqr.2	|- ( ph -> C = A )

Assertion

Ref	Expression
syl5sseqr	|- ( ph -> B C_ C )

Proof of Theorem syl5sseqr

Step	Hyp	Ref	Expression
1		syl5sseqr.1	. . 3 |- B C_ A
2	1	a1i 11	. 2 |- ( ph -> B C_ A )
3		syl5sseqr.2	. 2 |- ( ph -> C = A )
4	2, 3	sseqtr4d 3642	1 |- ( ph -> B C_ C )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  unissint  4501  resdif  6157  fimacnv  6347  tfrlem5  7476  domss2  8119  dffi3  8337  cantnfp1lem3  8577  trcl  8604  tcid  8615  r1ordg  8641  r1sssuc  8646  ackbij1lem15  9056  cfsmolem  9092  isfin4-3  9137  fin1a2lem7  9228  wunex2  9560  wuncid  9565  trclfvlb  13749  rtrclreclem1  13798  fsumsplit  14471  o1fsum  14545  fprodsplit  14696  phimullem  15484  vdwlem6  15690  ressinbas  15936  mrcssid  16277  mreexexlem2d  16305  acsfiindd  17177  dirge  17237  symgbasfi  17806  efgredlemf  18154  efgredlemd  18157  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumadd  18323  gsumzsplit  18327  gsumsplit2  18329  dprd2da  18441  dmdprdsplit2lem  18444  dmdprdsplit2  18445  dmdprdsplit  18446  dprdsplit  18447  invrpropd  18698  issubdrg  18805  lspssid  18985  aspssid  19333  pjcss  20060  istopon  20717  sscls  20860  ordtbas  20996  cncls2  21077  tgcmp  21204  cmpfi  21211  1stcfb  21248  1stckgenlem  21356  ptbasfi  21384  ptcnplem  21424  ptuncnv  21610  ptunhmeo  21611  fbasrn  21688  cnflf2  21807  fclscmp  21834  alexsublem  21848  ghmcnp  21918  tsmsgsum  21942  tsmsres  21947  tsmssplit  21955  tsmsxplem1  21956  ustssco  22018  mopnfss  22248  cnmpt2pc  22727  uniiccdif  23346  uniioombllem3  23353  uniioombllem4  23354  itg2splitlem  23515  itg2split  23516  itgsplit  23602  ellimc2  23641  ellimc3  23643  lhop  23779  plyaddlem1  23969  plymullem1  23970  taylthlem2  24128  mtest  24158  xrlimcnp  24695  fsumharmonic  24738  chtdif  24884  dchrghm  24981  lgsquadlem2  25106  dchrisumlema  25177  dchrisumlem2  25179  dchrisum0lem1b  25204  dchrisum0lem1  25205  pntrlog2bndlem6  25272  pntlemf  25294  umgr2adedgwlk  26841  umgr2adedgwlkon  26842  umgr2adedgspth  26844  ex-res  27298  spanss2  28204  mdsymi  29270  padct  29497  ordtconnlem1  29970  issgon  30186  sssigagen  30208  measiuns  30280  sitgclg  30404  cvmliftlem10  31276  ftc1anclem6  33490  heibor1lem  33608  heibor  33620  divrngcl  33756  isdrngo2  33757  igenss  33861  paddunssN  35094  sspadd1  35101  sspadd2  35102  pclssidN  35181  diassdvaN  36349  dochvalr  36646  lcdvbase  36882  nacsfix  37275  isnumbasgrplem2  37674  rgspnssid  37740  itgpowd  37800  trrelsuperrel2dg  37963  fvilbd  37981  relexp0a  38008  wnefimgd  38460  icccncfext  40100  iblsplit  40182  dirkeritg  40319  dirkercncflem2  40321  fourierdlem81  40404  fourierdlem89  40412  fourierdlem91  40414  fourierdlem92  40415  fourierdlem111  40434  fouriercn  40449  hspdifhsp  40830  srhmsubc  42076  srhmsubcALTV  42094  gsumsplit2f  42143  fdivmpt  42334  fdivpm  42337  refdivpm  42338  elpglem2  42455