Theorem sseqtrrdi 3972

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  3sstr4g  3984  abssdv  4015  disjxiun  5100  knatar  7359  iunpw  7774  fviunfun  7946  frrlem8  8295  frrlem10  8297  frrlem12  8299  frrlem14  8301  fprresex  8312  tfrlem9  8377  tfrlem9a  8378  tfrlem13  8382  tz7.44-2  8399  tz7.44-3  8400  tz7.49  8439  naddcllem  8669  naddov2  8672  naddasslem1  8688  naddasslem2  8689  marypha1lem  9409  ordtypelem2  9497  ixpiunwdom  9568  oemapvali  9669  tcss  9727  tcel  9728  pwwf  9797  rankpwi  9813  rankval3b  9817  cplem1  9931  cplem1OLD  9932  setrec1  9953  dfac12lem2  10204  infmap2  10276  ackbij1b  10297  ttukeylem6  10573  fpwwe2lem10  10706  fpwwe2lem11  10707  fpwwe2lem12  10708  fpwwe2  10709  uznnssnn  13003  pfxccatpfx2  14866  shftfval  15203  rexuzre  15500  climsup  15817  clim2prod  16037  fprodntriv  16089  eulerthlem2  16939  ramtlecl  17158  mreexexlem4d  17801  mreexdomd  17803  gsumpropd2lem  18848  gsumzaddlem  20115  gsum2d  20166  telgsums  20187  pgpfac1lem1  20270  pgpfac1lem3a  20272  pgpfac1lem3  20273  pgpfac1lem5  20275  lspsolvlem  21400  lbsextlem2  21417  dsmmacl  22027  lindsdom  22136  eltopss  23205  difopn  23332  tgrest  23457  perfopn  23483  pnfnei  23518  mnfnei  23519  regsep2  23674  cncmp  23690  uncmp  23701  hauscmplem  23704  hauscmp  23705  conndisj  23714  cnconn  23720  conncompss  23731  2ndcctbss  23754  islly2  23783  comppfsc  23831  1stckgenlem  23852  txuni2  23864  ptbasfi  23880  ptpjopn  23911  txindis  23933  txtube  23939  hausdiag  23944  xkoinjcn  23986  tgqtop  24011  filconn  24182  elfm2  24247  flimclslem  24283  flffbas  24294  fclsbas  24320  flimfnfcls  24327  alexsubALT  24350  symgtgp  24405  ustssco  24514  isucn2  24577  ucnima  24579  ucnprima  24580  blcls  24805  prdsxmslem2  24828  isngp2  24896  tgioo  25095  xrtgioo  25106  xrsmopn  25112  opnreen  25131  cnheiborlem  25255  cnllycmp  25257  tcphcph  25538  rrxmvallem  25705  uniioombllem4  25887  dyadmbllem  25900  opnmbllem  25902  mbfimaopnlem  25956  mbflimsup  25967  i1fadd  25996  i1fmul  25997  itg1addlem4  26000  i1fmulc  26004  limciun  26194  dvlip2  26295  c1lip3  26299  lhop  26316  dvfsumlem2  26327  dvfsumrlimge0  26330  dvfsumrlim2  26332  ulmval  26689  psercnlem2  26733  efopnlem2  26967  efopn  26968  madebdayim  28256  madefi  28281  oldfi  28282  addbdaylem  28385  oniso  28639  oldfib  28745  lfuhgr  29708  umgrres1lem  29873  upgrres1  29876  nbgrssvwo2  29925  ubthlem1  31454  issh2  31793  mdsymlem1  32987  iunxpssiun1  33144  padct  33292  xrofsup  33341  fz2ssnn0  33359  ccatws1f1o  33496  elrgspnlem1  33785  unitpidl1  33956  mxidlirred  33979  zarclsint  34486  tpr2rico  34526  sibfinima  34954  fct2relem  35209  bnj906  35543  bnj1014  35574  bnj1286  35632  bnj1408  35649  bnj1450  35663  bnj1452  35665  bnj1498  35674  bnj1501  35680  vonf1oonfo  35867  cvmopnlem  36012  cvmfolem  36013  cvmliftlem6  36024  cvmliftlem8  36026  cvmliftlem13  36030  cvmliftlem15  36032  cvmlift2lem9  36045  cvmlift2lem11  36047  cvmlift2lem12  36048  mclsppslem  36317  filnetlem4  37139  dissneqlem  38231  pibt2  38308  opnmbllem0  38542  cnambfre  38554  heibor1lem  38711  osumcllem1N  40981  osumcllem2N  40982  pexmidlem6N  41000  dochexmidlem6  42490  dochexmidlem7  42491  mapdrvallem3  42671  evlsmhpvvval  43585  naddwordnexlem4  44361  k0004ss2  45111  cpcolld  45201  dvsconst  45273  dvsid  45274  dvsef  45275  iunconnlem2  45876  uzssd2  46371  climinf  46562  climsuse  46564  climresmpt  46613  climleltrp  46630  stoweidlem28  46982  stoweidlem50  47004  stoweidlem52  47006  stoweidlem53  47007  stoweidlem54  47008  fourierdlem54  47114  fourierdlem80  47140  meaiininclem  47440  caratheodorylem2  47481  hspmbllem2  47581  mbfresmf  47693  smfmbfcex  47714  smflimlem2  47726  smflimsuplem2  47775  smflimsuplem3  47776  smflimsuplem5  47778  smflimsuplem6  47779  gpgedgvtx1lem  48349  isuspgrim0  48936  gpgusgralem  49098  upgredgssspr  49185  setrecsres  50739  aacllem  50883