Theorem syl6sseqr 3877

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

Ref	Expression
syl6sseqr	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl6sseqr

Step	Hyp	Ref	Expression
1		syl6ssr.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		syl6ssr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2834	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6sseq 3876	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1656   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812

This theorem is referenced by:  disjxiun  4870  knatar  6862  iunpw  7239  wfrdmcl  7689  wfrlem12  7692  wfrlem16  7696  wfrlem17  7697  tfrlem9  7747  tfrlem9a  7748  tfrlem13  7752  tz7.44-2  7769  tz7.44-3  7770  tz7.49  7806  marypha1lem  8608  ordtypelem2  8693  ixpiunwdom  8765  oemapvali  8858  tcss  8897  tcel  8898  pwwf  8947  rankpwi  8963  rankval3b  8966  cplem1  9029  dfac12lem2  9281  infmap2  9355  ackbij1b  9376  ttukeylem6  9651  fpwwe2lem11  9777  fpwwe2lem12  9778  fpwwe2lem13  9779  fpwwe2  9780  uznnssnn  12017  pfxccatpfx2  13838  shftfval  14187  rexuzre  14469  climsup  14777  clim2prod  14993  fprodntriv  15045  eulerthlem2  15858  ramtlecl  16075  mreexexlem4d  16660  mreexdomd  16662  gsumpropd2lem  17626  gsumzaddlem  18674  gsum2d  18724  telgsums  18744  pgpfac1lem1  18827  pgpfac1lem3a  18829  pgpfac1lem3  18830  pgpfac1lem5  18832  lspsolvlem  19502  lbsextlem2  19520  dsmmacl  20448  eltopss  21082  difopn  21209  tgrest  21334  perfopn  21360  pnfnei  21395  mnfnei  21396  regsep2  21551  cncmp  21566  uncmp  21577  hauscmplem  21580  hauscmp  21581  conndisj  21590  cnconn  21596  conncompss  21607  2ndcctbss  21629  islly2  21658  comppfsc  21706  1stckgenlem  21727  txuni2  21739  ptbasfi  21755  ptpjopn  21786  txindis  21808  txtube  21814  hausdiag  21819  xkoinjcn  21861  tgqtop  21886  filconn  22057  elfm2  22122  flimclslem  22158  flffbas  22169  fclsbas  22195  flimfnfcls  22202  alexsubALT  22225  symgtgp  22275  ustssco  22388  isucn2  22453  ucnima  22455  ucnprima  22456  blcls  22681  prdsxmslem2  22704  isngp2  22771  tgioo  22969  xrtgioo  22979  xrsmopn  22985  opnreen  23004  cnheiborlem  23123  cnllycmp  23125  tcphcph  23405  rrxmvallem  23572  uniioombllem4  23752  dyadmbllem  23765  opnmbllem  23767  mbfimaopnlem  23821  mbflimsup  23832  i1fadd  23861  i1fmul  23862  itg1addlem4  23865  i1fmulc  23869  limciun  24057  dvlip2  24157  c1lip3  24161  lhop  24178  dvfsumlem2  24189  dvfsumrlimge0  24192  dvfsumrlim2  24194  ulmval  24533  psercnlem2  24577  efopnlem2  24802  efopn  24803  umgrres1lem  26607  upgrres1  26610  nbgrssvwo2  26659  ubthlem1  28270  issh2  28610  mdsymlem1  29806  padct  30034  xrofsup  30069  fz2ssnn0  30083  tpr2rico  30492  sibfinima  30935  fct2relem  31213  bnj906  31535  bnj1014  31565  bnj1286  31622  bnj1408  31639  bnj1450  31653  bnj1452  31655  bnj1498  31664  bnj1501  31670  cvmopnlem  31795  cvmfolem  31796  cvmliftlem6  31807  cvmliftlem8  31809  cvmliftlem13  31813  cvmliftlem15  31815  cvmlift2lem9  31828  cvmlift2lem11  31830  cvmlift2lem12  31831  mclsppslem  32015  trpredpred  32255  trpredtr  32257  trpredrec  32265  frrlem5e  32316  frrlem11  32320  filnetlem4  32903  dissneqlem  33726  lindsdom  33940  opnmbllem0  33982  cnambfre  33994  heibor1lem  34143  osumcllem1N  36024  osumcllem2N  36025  pexmidlem6N  36043  dochexmidlem6  37533  dochexmidlem7  37534  mapdrvallem3  37714  k0004ss2  39283  dvsconst  39362  dvsid  39363  dvsef  39364  iunconnlem2  39982  uzssd2  40432  climinf  40626  climsuse  40628  climresmpt  40679  climleltrp  40696  stoweidlem28  41032  stoweidlem50  41054  stoweidlem52  41056  stoweidlem53  41057  stoweidlem54  41058  fourierdlem54  41164  fourierdlem80  41190  meaiininclem  41487  caratheodorylem2  41528  hspmbllem2  41628  mbfresmf  41735  smfmbfcex  41755  smflimlem2  41767  smflimsuplem2  41814  smflimsuplem3  41815  smflimsuplem5  41817  smflimsuplem6  41818  isomuspgrlem2c  42541  upgredgssspr  42591  setrec1  43326  setrecsres  43336  aacllem  43436