Theorem sseqtrrdi 4018

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  disjxiun  5063  knatar  7110  iunpw  7493  fviunfun  7646  wfrdmcl  7963  wfrlem12  7966  wfrlem16  7970  wfrlem17  7971  tfrlem9  8021  tfrlem9a  8022  tfrlem13  8026  tz7.44-2  8043  tz7.44-3  8044  tz7.49  8081  marypha1lem  8897  ordtypelem2  8983  ixpiunwdom  9055  oemapvali  9147  tcss  9186  tcel  9187  pwwf  9236  rankpwi  9252  rankval3b  9255  cplem1  9318  dfac12lem2  9570  infmap2  9640  ackbij1b  9661  ttukeylem6  9936  fpwwe2lem11  10062  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  uznnssnn  12296  pfxccatpfx2  14099  shftfval  14429  rexuzre  14712  climsup  15026  clim2prod  15244  fprodntriv  15296  eulerthlem2  16119  ramtlecl  16336  mreexexlem4d  16918  mreexdomd  16920  gsumpropd2lem  17889  gsumzaddlem  19041  gsum2d  19092  telgsums  19113  pgpfac1lem1  19196  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfac1lem5  19201  lspsolvlem  19914  lbsextlem2  19931  dsmmacl  20885  eltopss  21515  difopn  21642  tgrest  21767  perfopn  21793  pnfnei  21828  mnfnei  21829  regsep2  21984  cncmp  22000  uncmp  22011  hauscmplem  22014  hauscmp  22015  conndisj  22024  cnconn  22030  conncompss  22041  2ndcctbss  22063  islly2  22092  comppfsc  22140  1stckgenlem  22161  txuni2  22173  ptbasfi  22189  ptpjopn  22220  txindis  22242  txtube  22248  hausdiag  22253  xkoinjcn  22295  tgqtop  22320  filconn  22491  elfm2  22556  flimclslem  22592  flffbas  22603  fclsbas  22629  flimfnfcls  22636  alexsubALT  22659  symgtgp  22714  ustssco  22823  isucn2  22888  ucnima  22890  ucnprima  22891  blcls  23116  prdsxmslem2  23139  isngp2  23206  tgioo  23404  xrtgioo  23414  xrsmopn  23420  opnreen  23439  cnheiborlem  23558  cnllycmp  23560  tcphcph  23840  rrxmvallem  24007  uniioombllem4  24187  dyadmbllem  24200  opnmbllem  24202  mbfimaopnlem  24256  mbflimsup  24267  i1fadd  24296  i1fmul  24297  itg1addlem4  24300  i1fmulc  24304  limciun  24492  dvlip2  24592  c1lip3  24596  lhop  24613  dvfsumlem2  24624  dvfsumrlimge0  24627  dvfsumrlim2  24629  ulmval  24968  psercnlem2  25012  efopnlem2  25240  efopn  25241  umgrres1lem  27092  upgrres1  27095  nbgrssvwo2  27144  ubthlem1  28647  issh2  28986  mdsymlem1  30180  padct  30455  xrofsup  30492  fz2ssnn0  30508  tpr2rico  31155  sibfinima  31597  fct2relem  31868  bnj906  32202  bnj1014  32233  bnj1286  32291  bnj1408  32308  bnj1450  32322  bnj1452  32324  bnj1498  32333  bnj1501  32339  lfuhgr  32364  cvmopnlem  32525  cvmfolem  32526  cvmliftlem6  32537  cvmliftlem8  32539  cvmliftlem13  32543  cvmliftlem15  32545  cvmlift2lem9  32558  cvmlift2lem11  32560  cvmlift2lem12  32561  mclsppslem  32830  trpredpred  33067  trpredtr  33069  trpredrec  33077  frrlem8  33130  frrlem10  33132  frrlem12  33134  frrlem14  33136  filnetlem4  33729  dissneqlem  34624  pibt2  34701  lindsdom  34901  opnmbllem0  34943  cnambfre  34955  heibor1lem  35102  osumcllem1N  37107  osumcllem2N  37108  pexmidlem6N  37126  dochexmidlem6  38616  dochexmidlem7  38617  mapdrvallem3  38797  k0004ss2  40522  cpcolld  40614  dvsconst  40682  dvsid  40683  dvsef  40684  iunconnlem2  41289  uzssd2  41711  climinf  41907  climsuse  41909  climresmpt  41960  climleltrp  41977  stoweidlem28  42333  stoweidlem50  42355  stoweidlem52  42357  stoweidlem53  42358  stoweidlem54  42359  fourierdlem54  42465  fourierdlem80  42491  meaiininclem  42788  caratheodorylem2  42829  hspmbllem2  42929  mbfresmf  43036  smfmbfcex  43056  smflimlem2  43068  smflimsuplem2  43115  smflimsuplem3  43116  smflimsuplem5  43118  smflimsuplem6  43119  isomuspgrlem2c  44015  upgredgssspr  44038  setrec1  44814  setrecsres  44824  aacllem  44922