Theorem syl5sseqr 3904

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

Hypotheses

Ref	Expression
syl5sseqr.1	⊢ 𝐵 ⊆ 𝐴
syl5sseqr.2	⊢ (𝜑 → 𝐶 = 𝐴)

Assertion

Ref	Expression
syl5sseqr	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem syl5sseqr

Step	Hyp	Ref	Expression
1		syl5sseqr.1	. . 3 ⊢ 𝐵 ⊆ 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		syl5sseqr.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
4	2, 3	sseqtr4d 3892	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1507   ⊆ wss 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-in 3830  df-ss 3837

This theorem is referenced by:  unissint  4767  resdif  6458  fimacnv  6658  tfrlem5  7814  domss2  8466  dffi3  8684  cantnfp1lem3  8931  trcl  8958  tcid  8969  r1ordg  8995  r1sssuc  9000  ackbij1lem15  9448  cfsmolem  9484  fin1a2lem7  9620  wunex2  9952  wuncid  9957  trclfvlb  14223  rtrclreclem1  14272  fsumsplit  14951  o1fsum  15022  fprodsplit  15174  phimullem  15966  vdwlem6  16172  ressinbas  16410  mrcssid  16740  mreexexlem2d  16768  acsfiindd  17639  dirge  17699  symgbasfi  18269  efgredlemf  18620  efgredlemd  18623  gsumzres  18777  gsumzcl2  18778  gsumzf1o  18780  gsumadd  18790  gsumzsplit  18794  gsumsplit2  18796  dprd2da  18908  dmdprdsplit2lem  18911  dmdprdsplit2  18912  dmdprdsplit  18913  dprdsplit  18914  invrpropd  19165  issubdrg  19277  lspssid  19473  aspssid  19821  pjcss  20556  istopon  21218  sscls  21362  ordtbas  21498  cncls2  21579  tgcmp  21707  cmpfi  21714  1stcfb  21751  1stckgenlem  21859  ptbasfi  21887  ptcnplem  21927  ptuncnv  22113  ptunhmeo  22114  fbasrn  22190  cnflf2  22309  fclscmp  22336  alexsublem  22350  ghmcnp  22420  tsmsgsum  22444  tsmsres  22449  tsmssplit  22457  tsmsxplem1  22458  ustssco  22520  mopnfss  22750  cnmpopc  23229  uniiccdif  23876  uniioombllem3  23883  uniioombllem4  23884  itg2splitlem  24046  itg2split  24047  itgsplit  24133  ellimc2  24172  ellimc3  24174  lhop  24310  plyaddlem1  24500  plymullem1  24501  taylthlem2  24659  mtest  24689  xrlimcnp  25242  fsumharmonic  25285  chtdif  25431  dchrghm  25528  lgsquadlem2  25653  dchrisumlema  25760  dchrisumlem2  25762  dchrisum0lem1b  25787  dchrisum0lem1  25788  pntrlog2bndlem6  25855  pntlemf  25877  nbupgruvtxres  26886  umgr2adedgwlk  27445  umgr2adedgwlkon  27446  umgr2adedgspth  27448  ex-res  27992  spanss2  28897  mdsymi  29963  padct  30208  ordtconnlem1  30811  issgon  31027  sssigagen  31049  measiuns  31121  sitgclg  31245  cvmliftlem10  32126  rdgssun  34101  ftc1anclem6  34413  heibor1lem  34529  heibor  34541  divrngcl  34677  isdrngo2  34678  igenss  34782  paddunssN  36389  sspadd1  36396  sspadd2  36397  pclssidN  36476  diassdvaN  37641  dochvalr  37938  lcdvbase  38174  nacsfix  38704  isnumbasgrplem2  39100  rgspnssid  39166  itgpowd  39217  trrelsuperrel2dg  39379  fvilbd  39397  relexp0a  39424  wnefimgd  39875  grumnudlem  39996  icccncfext  41600  iblsplit  41681  dirkeritg  41818  dirkercncflem2  41820  fourierdlem81  41903  fourierdlem89  41911  fourierdlem91  41913  fourierdlem92  41914  fourierdlem111  41933  fouriercn  41948  hspdifhsp  42329  srhmsubc  43711  srhmsubcALTV  43729  gsumsplit2f  43776  fdivmpt  43968  fdivpm  43971  refdivpm  43972  elpglem2  44181