Theorem sseqtrrdi 3975

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrdi

Step	Hyp	Ref	Expression
1		sseqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2745	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtrdi 3974	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  3sstr4g  3987  abssdv  4019  disjxiun  5095  knatar  7303  iunpw  7716  fviunfun  7889  frrlem8  8235  frrlem10  8237  frrlem12  8239  frrlem14  8241  fprresex  8252  tfrlem9  8316  tfrlem9a  8317  tfrlem13  8321  tz7.44-2  8338  tz7.44-3  8339  tz7.49  8376  naddcllem  8604  naddov2  8607  naddasslem1  8622  naddasslem2  8623  marypha1lem  9336  ordtypelem2  9424  ixpiunwdom  9495  oemapvali  9593  tcss  9651  tcel  9652  pwwf  9719  rankpwi  9735  rankval3b  9738  cplem1  9801  dfac12lem2  10055  infmap2  10127  ackbij1b  10148  ttukeylem6  10424  fpwwe2lem10  10551  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  uznnssnn  12808  pfxccatpfx2  14660  shftfval  14993  rexuzre  15276  climsup  15593  clim2prod  15811  fprodntriv  15865  eulerthlem2  16709  ramtlecl  16928  mreexexlem4d  17570  mreexdomd  17572  gsumpropd2lem  18604  gsumzaddlem  19850  gsum2d  19901  telgsums  19922  pgpfac1lem1  20005  pgpfac1lem3a  20007  pgpfac1lem3  20008  pgpfac1lem5  20010  lspsolvlem  21097  lbsextlem2  21114  dsmmacl  21696  eltopss  22851  difopn  22978  tgrest  23103  perfopn  23129  pnfnei  23164  mnfnei  23165  regsep2  23320  cncmp  23336  uncmp  23347  hauscmplem  23350  hauscmp  23351  conndisj  23360  cnconn  23366  conncompss  23377  2ndcctbss  23399  islly2  23428  comppfsc  23476  1stckgenlem  23497  txuni2  23509  ptbasfi  23525  ptpjopn  23556  txindis  23578  txtube  23584  hausdiag  23589  xkoinjcn  23631  tgqtop  23656  filconn  23827  elfm2  23892  flimclslem  23928  flffbas  23939  fclsbas  23965  flimfnfcls  23972  alexsubALT  23995  symgtgp  24050  ustssco  24159  isucn2  24222  ucnima  24224  ucnprima  24225  blcls  24450  prdsxmslem2  24473  isngp2  24541  tgioo  24740  xrtgioo  24751  xrsmopn  24757  opnreen  24776  cnheiborlem  24909  cnllycmp  24911  tcphcph  25193  rrxmvallem  25360  uniioombllem4  25543  dyadmbllem  25556  opnmbllem  25558  mbfimaopnlem  25612  mbflimsup  25623  i1fadd  25652  i1fmul  25653  itg1addlem4  25656  i1fmulc  25660  limciun  25851  dvlip2  25956  c1lip3  25960  lhop  25977  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumrlimge0  25993  dvfsumrlim2  25995  ulmval  26345  psercnlem2  26390  efopnlem2  26622  efopn  26623  madebdayim  27884  madefi  27909  oldfi  27910  addbdaylem  28013  oniso  28267  oldfib  28373  umgrres1lem  29383  upgrres1  29386  nbgrssvwo2  29435  ubthlem1  30945  issh2  31284  mdsymlem1  32478  iunxpssiun1  32643  padct  32797  xrofsup  32847  fz2ssnn0  32865  ccatws1f1o  33033  elrgspnlem1  33324  unitpidl1  33505  mxidlirred  33553  zarclsint  34029  tpr2rico  34069  sibfinima  34496  fct2relem  34754  bnj906  35086  bnj1014  35117  bnj1286  35175  bnj1408  35192  bnj1450  35206  bnj1452  35208  bnj1498  35217  bnj1501  35223  lfuhgr  35312  cvmopnlem  35472  cvmfolem  35473  cvmliftlem6  35484  cvmliftlem8  35486  cvmliftlem13  35490  cvmliftlem15  35492  cvmlift2lem9  35505  cvmlift2lem11  35507  cvmlift2lem12  35508  mclsppslem  35777  filnetlem4  36575  dissneqlem  37541  pibt2  37618  lindsdom  37811  opnmbllem0  37853  cnambfre  37865  heibor1lem  38006  osumcllem1N  40212  osumcllem2N  40213  pexmidlem6N  40231  dochexmidlem6  41721  dochexmidlem7  41722  mapdrvallem3  41902  evlsmhpvvval  42834  naddwordnexlem4  43639  k0004ss2  44389  cpcolld  44495  dvsconst  44567  dvsid  44568  dvsef  44569  iunconnlem2  45171  uzssd2  45657  climinf  45848  climsuse  45850  climresmpt  45899  climleltrp  45916  stoweidlem28  46268  stoweidlem50  46290  stoweidlem52  46292  stoweidlem53  46293  stoweidlem54  46294  fourierdlem54  46400  fourierdlem80  46426  meaiininclem  46726  caratheodorylem2  46767  hspmbllem2  46867  mbfresmf  46979  smfmbfcex  47000  smflimlem2  47012  smflimsuplem2  47061  smflimsuplem3  47062  smflimsuplem5  47064  smflimsuplem6  47065  gpgedgvtx1lem  47573  isuspgrim0  48136  gpgusgralem  48298  upgredgssspr  48385  setrec1  49932  setrecsres  49943  aacllem  50042