Theorem syl6sseqr 3615

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 2619	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6sseq 3614	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  disjxiun  4579  disjxiunOLD  4580  knatar  6507  iunpw  6870  wfrdmcl  7310  wfrlem12  7313  wfrlem16  7317  wfrlem17  7318  tfrlem9  7368  tfrlem9a  7369  tfrlem13  7373  tz7.44-2  7390  tz7.44-3  7391  tz7.49  7427  marypha1lem  8222  ordtypelem2  8307  ixpiunwdom  8379  oemapvali  8464  tcss  8503  tcel  8504  pwwf  8553  rankpwi  8569  rankval3b  8572  cplem1  8635  dfac12lem2  8849  infmap2  8923  ackbij1b  8944  ttukeylem6  9219  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  uznnssnn  11611  shftfval  13658  rexuzre  13940  climsup  14248  clim2prod  14459  fprodntriv  14511  eulerthlem2  15325  ramtlecl  15542  mreexexlem4d  16130  mreexdomd  16133  gsumpropd2lem  17096  gsumzaddlem  18144  gsum2d  18194  telgsums  18213  pgpfac1lem1  18296  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfac1lem5  18301  lspsolvlem  18963  lbsextlem2  18980  dsmmacl  19904  eltopss  20537  difopn  20648  tgrest  20773  perfopn  20799  pnfnei  20834  mnfnei  20835  regsep2  20990  cncmp  21005  uncmp  21016  hauscmplem  21019  hauscmp  21020  conndisj  21029  cnconn  21035  concompss  21046  2ndcctbss  21068  islly2  21097  comppfsc  21145  1stckgenlem  21166  txuni2  21178  ptbasfi  21194  ptpjopn  21225  txindis  21247  txtube  21253  hausdiag  21258  xkoinjcn  21300  tgqtop  21325  filcon  21497  elfm2  21562  flimclslem  21598  flffbas  21609  fclsbas  21635  flimfnfcls  21642  alexsubALT  21665  symgtgp  21715  ustssco  21828  isucn2  21893  ucnima  21895  ucnprima  21896  blcls  22121  prdsxmslem2  22144  isngp2  22211  tgioo  22407  xrtgioo  22417  xrsmopn  22423  opnreen  22442  cnheiborlem  22561  cnllycmp  22563  tchcph  22844  rrxmvallem  22995  uniioombllem4  23160  dyadmbllem  23173  opnmbllem  23175  mbfimaopnlem  23228  mbflimsup  23239  i1fadd  23268  i1fmul  23269  itg1addlem4  23272  i1fmulc  23276  limciun  23464  dvlip2  23562  c1lip3  23566  lhop  23583  dvfsumlem2  23594  dvfsumrlimge0  23597  dvfsumrlim2  23599  ulmval  23938  psercnlem2  23982  efopnlem2  24203  efopn  24204  nbgrassvwo2  25967  ubthlem1  27110  issh2  27450  mdsymlem1  28646  padct  28885  xrofsup  28923  tpr2rico  29286  sibfinima  29728  bnj906  30254  bnj1014  30284  bnj1286  30341  bnj1408  30358  bnj1450  30372  bnj1452  30374  bnj1498  30383  bnj1501  30389  cvmopnlem  30514  cvmfolem  30515  cvmliftlem6  30526  cvmliftlem8  30528  cvmliftlem13  30532  cvmliftlem15  30534  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift2lem12  30550  mclsppslem  30734  trpredpred  30972  trpredtr  30974  trpredrec  30982  frrlem5e  31032  frrlem11  31036  filnetlem4  31546  dissneqlem  32363  lindsdom  32573  opnmbllem0  32615  cnambfre  32628  heibor1lem  32778  osumcllem1N  34260  osumcllem2N  34261  pexmidlem6N  34279  dochexmidlem6  35772  dochexmidlem7  35773  mapdrvallem3  35953  k0004ss2  37470  dvsconst  37551  dvsid  37552  dvsef  37553  iunconlem2  38193  climinf  38673  climsuse  38675  climresmpt  38726  climleltrp  38743  stoweidlem28  38921  stoweidlem50  38943  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  fourierdlem54  39053  fourierdlem80  39079  meaiininclem  39376  caratheodorylem2  39417  hspmbllem2  39517  mbfresmf  39626  smfmbfcex  39646  smflimlem2  39658  pfxccatpfx2  40291  umgrres1lem  40529  upgrres1  40532  nbgrssvwo2  40587  setrec1  42237  aacllem  42356