Theorem syl6sseqr 3652

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

Syntax hints:   → wi 4   = wceq 1483   ⊆ 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:  disjxiun  4649  disjxiunOLD  4650  knatar  6607  iunpw  6978  wfrdmcl  7423  wfrlem12  7426  wfrlem16  7430  wfrlem17  7431  tfrlem9  7481  tfrlem9a  7482  tfrlem13  7486  tz7.44-2  7503  tz7.44-3  7504  tz7.49  7540  marypha1lem  8339  ordtypelem2  8424  ixpiunwdom  8496  oemapvali  8581  tcss  8620  tcel  8621  pwwf  8670  rankpwi  8686  rankval3b  8689  cplem1  8752  dfac12lem2  8966  infmap2  9040  ackbij1b  9061  ttukeylem6  9336  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  uznnssnn  11735  shftfval  13810  rexuzre  14092  climsup  14400  clim2prod  14620  fprodntriv  14672  eulerthlem2  15487  ramtlecl  15704  mreexexlem4d  16307  mreexdomd  16310  gsumpropd2lem  17273  gsumzaddlem  18321  gsum2d  18371  telgsums  18390  pgpfac1lem1  18473  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem5  18478  lspsolvlem  19142  lbsextlem2  19159  dsmmacl  20085  eltopss  20712  difopn  20838  tgrest  20963  perfopn  20989  pnfnei  21024  mnfnei  21025  regsep2  21180  cncmp  21195  uncmp  21206  hauscmplem  21209  hauscmp  21210  conndisj  21219  cnconn  21225  conncompss  21236  2ndcctbss  21258  islly2  21287  comppfsc  21335  1stckgenlem  21356  txuni2  21368  ptbasfi  21384  ptpjopn  21415  txindis  21437  txtube  21443  hausdiag  21448  xkoinjcn  21490  tgqtop  21515  filconn  21687  elfm2  21752  flimclslem  21788  flffbas  21799  fclsbas  21825  flimfnfcls  21832  alexsubALT  21855  symgtgp  21905  ustssco  22018  isucn2  22083  ucnima  22085  ucnprima  22086  blcls  22311  prdsxmslem2  22334  isngp2  22401  tgioo  22599  xrtgioo  22609  xrsmopn  22615  opnreen  22634  cnheiborlem  22753  cnllycmp  22755  tchcph  23036  rrxmvallem  23187  uniioombllem4  23354  dyadmbllem  23367  opnmbllem  23369  mbfimaopnlem  23422  mbflimsup  23433  i1fadd  23462  i1fmul  23463  itg1addlem4  23466  i1fmulc  23470  limciun  23658  dvlip2  23758  c1lip3  23762  lhop  23779  dvfsumlem2  23790  dvfsumrlimge0  23793  dvfsumrlim2  23795  ulmval  24134  psercnlem2  24178  efopnlem2  24403  efopn  24404  umgrres1lem  26202  upgrres1  26205  nbgrssvwo2  26261  ubthlem1  27726  issh2  28066  mdsymlem1  29262  padct  29497  xrofsup  29533  fz2ssnn0  29547  tpr2rico  29958  sibfinima  30401  fct2relem  30675  bnj906  31000  bnj1014  31030  bnj1286  31087  bnj1408  31104  bnj1450  31118  bnj1452  31120  bnj1498  31129  bnj1501  31135  cvmopnlem  31260  cvmfolem  31261  cvmliftlem6  31272  cvmliftlem8  31274  cvmliftlem13  31278  cvmliftlem15  31280  cvmlift2lem9  31293  cvmlift2lem11  31295  cvmlift2lem12  31296  mclsppslem  31480  trpredpred  31728  trpredtr  31730  trpredrec  31738  frrlem5e  31788  frrlem11  31792  filnetlem4  32376  dissneqlem  33187  lindsdom  33403  opnmbllem0  33445  cnambfre  33458  heibor1lem  33608  osumcllem1N  35242  osumcllem2N  35243  pexmidlem6N  35261  dochexmidlem6  36754  dochexmidlem7  36755  mapdrvallem3  36935  k0004ss2  38450  dvsconst  38529  dvsid  38530  dvsef  38531  iunconnlem2  39171  uzssd2  39644  climinf  39838  climsuse  39840  climresmpt  39891  climleltrp  39908  stoweidlem28  40245  stoweidlem50  40267  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  fourierdlem54  40377  fourierdlem80  40403  meaiininclem  40700  caratheodorylem2  40741  hspmbllem2  40841  mbfresmf  40948  smfmbfcex  40968  smflimlem2  40980  smflimsuplem2  41027  smflimsuplem3  41028  smflimsuplem5  41030  smflimsuplem6  41031  pfxccatpfx2  41428  upgredgssspr  41751  setrec1  42438  aacllem  42547