Theorem sseqtrrdi 3966

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  disjxiun  5027  knatar  7089  iunpw  7473  fviunfun  7628  wfrdmcl  7946  wfrlem12  7949  wfrlem16  7953  wfrlem17  7954  tfrlem9  8004  tfrlem9a  8005  tfrlem13  8009  tz7.44-2  8026  tz7.44-3  8027  tz7.49  8064  marypha1lem  8881  ordtypelem2  8967  ixpiunwdom  9038  oemapvali  9131  tcss  9170  tcel  9171  pwwf  9220  rankpwi  9236  rankval3b  9239  cplem1  9302  dfac12lem2  9555  infmap2  9629  ackbij1b  9650  ttukeylem6  9925  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  uznnssnn  12283  pfxccatpfx2  14090  shftfval  14421  rexuzre  14704  climsup  15018  clim2prod  15236  fprodntriv  15288  eulerthlem2  16109  ramtlecl  16326  mreexexlem4d  16910  mreexdomd  16912  gsumpropd2lem  17881  gsumzaddlem  19034  gsum2d  19085  telgsums  19106  pgpfac1lem1  19189  pgpfac1lem3a  19191  pgpfac1lem3  19192  pgpfac1lem5  19194  lspsolvlem  19907  lbsextlem2  19924  dsmmacl  20430  eltopss  21512  difopn  21639  tgrest  21764  perfopn  21790  pnfnei  21825  mnfnei  21826  regsep2  21981  cncmp  21997  uncmp  22008  hauscmplem  22011  hauscmp  22012  conndisj  22021  cnconn  22027  conncompss  22038  2ndcctbss  22060  islly2  22089  comppfsc  22137  1stckgenlem  22158  txuni2  22170  ptbasfi  22186  ptpjopn  22217  txindis  22239  txtube  22245  hausdiag  22250  xkoinjcn  22292  tgqtop  22317  filconn  22488  elfm2  22553  flimclslem  22589  flffbas  22600  fclsbas  22626  flimfnfcls  22633  alexsubALT  22656  symgtgp  22711  ustssco  22820  isucn2  22885  ucnima  22887  ucnprima  22888  blcls  23113  prdsxmslem2  23136  isngp2  23203  tgioo  23401  xrtgioo  23411  xrsmopn  23417  opnreen  23436  cnheiborlem  23559  cnllycmp  23561  tcphcph  23841  rrxmvallem  24008  uniioombllem4  24190  dyadmbllem  24203  opnmbllem  24205  mbfimaopnlem  24259  mbflimsup  24270  i1fadd  24299  i1fmul  24300  itg1addlem4  24303  i1fmulc  24307  limciun  24497  dvlip2  24598  c1lip3  24602  lhop  24619  dvfsumlem2  24630  dvfsumrlimge0  24633  dvfsumrlim2  24635  ulmval  24975  psercnlem2  25019  efopnlem2  25248  efopn  25249  umgrres1lem  27100  upgrres1  27103  nbgrssvwo2  27152  ubthlem1  28653  issh2  28992  mdsymlem1  30186  padct  30481  xrofsup  30518  fz2ssnn0  30534  zarclsint  31225  tpr2rico  31265  sibfinima  31707  fct2relem  31978  bnj906  32312  bnj1014  32343  bnj1286  32401  bnj1408  32418  bnj1450  32432  bnj1452  32434  bnj1498  32443  bnj1501  32449  lfuhgr  32477  cvmopnlem  32638  cvmfolem  32639  cvmliftlem6  32650  cvmliftlem8  32652  cvmliftlem13  32656  cvmliftlem15  32658  cvmlift2lem9  32671  cvmlift2lem11  32673  cvmlift2lem12  32674  mclsppslem  32943  trpredpred  33180  trpredtr  33182  trpredrec  33190  frrlem8  33243  frrlem10  33245  frrlem12  33247  frrlem14  33249  filnetlem4  33842  dissneqlem  34757  pibt2  34834  lindsdom  35051  opnmbllem0  35093  cnambfre  35105  heibor1lem  35247  osumcllem1N  37252  osumcllem2N  37253  pexmidlem6N  37271  dochexmidlem6  38761  dochexmidlem7  38762  mapdrvallem3  38942  k0004ss2  40855  cpcolld  40966  dvsconst  41034  dvsid  41035  dvsef  41036  iunconnlem2  41641  uzssd2  42054  climinf  42248  climsuse  42250  climresmpt  42301  climleltrp  42318  stoweidlem28  42670  stoweidlem50  42692  stoweidlem52  42694  stoweidlem53  42695  stoweidlem54  42696  fourierdlem54  42802  fourierdlem80  42828  meaiininclem  43125  caratheodorylem2  43166  hspmbllem2  43266  mbfresmf  43373  smfmbfcex  43393  smflimlem2  43405  smflimsuplem2  43452  smflimsuplem3  43453  smflimsuplem5  43455  smflimsuplem6  43456  isomuspgrlem2c  44348  upgredgssspr  44371  setrec1  45221  setrecsres  45231  aacllem  45329