Theorem sseqtrrdi 3981

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  3sstr4g  3993  abssdv  4024  disjxiun  5111  knatar  7368  iunpw  7779  fviunfun  7951  frrlem8  8299  frrlem10  8301  frrlem12  8303  frrlem14  8305  fprresex  8316  tfrlem9  8381  tfrlem9a  8382  tfrlem13  8386  tz7.44-2  8403  tz7.44-3  8404  tz7.49  8441  naddcllem  8671  naddov2  8674  naddasslem1  8690  naddasslem2  8691  marypha1lem  9403  ordtypelem2  9491  ixpiunwdom  9562  oemapvali  9663  tcss  9721  tcel  9722  pwwf  9789  rankpwi  9805  rankval3b  9808  cplem1  9889  cplem1OLD  9890  dfac12lem2  10147  infmap2  10219  ackbij1b  10240  ttukeylem6  10516  fpwwe2lem10  10643  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  uznnssnn  12937  pfxccatpfx2  14798  shftfval  15133  rexuzre  15430  climsup  15747  clim2prod  15968  fprodntriv  16022  eulerthlem2  16866  ramtlecl  17085  mreexexlem4d  17728  mreexdomd  17730  gsumpropd2lem  18766  gsumzaddlem  20022  gsum2d  20073  telgsums  20094  pgpfac1lem1  20177  pgpfac1lem3a  20179  pgpfac1lem3  20180  pgpfac1lem5  20182  lspsolvlem  21303  lbsextlem2  21320  dsmmacl  21928  eltopss  23101  difopn  23228  tgrest  23353  perfopn  23379  pnfnei  23414  mnfnei  23415  regsep2  23570  cncmp  23586  uncmp  23597  hauscmplem  23600  hauscmp  23601  conndisj  23610  cnconn  23616  conncompss  23627  2ndcctbss  23649  islly2  23678  comppfsc  23726  1stckgenlem  23747  txuni2  23759  ptbasfi  23775  ptpjopn  23806  txindis  23828  txtube  23834  hausdiag  23839  xkoinjcn  23881  tgqtop  23906  filconn  24077  elfm2  24142  flimclslem  24178  flffbas  24189  fclsbas  24215  flimfnfcls  24222  alexsubALT  24245  symgtgp  24300  ustssco  24409  isucn2  24472  ucnima  24474  ucnprima  24475  blcls  24700  prdsxmslem2  24723  isngp2  24791  tgioo  24990  xrtgioo  25001  xrsmopn  25007  opnreen  25026  cnheiborlem  25150  cnllycmp  25152  tcphcph  25433  rrxmvallem  25600  uniioombllem4  25782  dyadmbllem  25795  opnmbllem  25797  mbfimaopnlem  25851  mbflimsup  25862  i1fadd  25891  i1fmul  25892  itg1addlem4  25895  i1fmulc  25899  limciun  26090  dvlip2  26191  c1lip3  26195  lhop  26212  dvfsumlem2  26223  dvfsumrlimge0  26226  dvfsumrlim2  26228  ulmval  26580  psercnlem2  26624  efopnlem2  26859  efopn  26860  madebdayim  28118  madefi  28143  oldfi  28144  addbdaylem  28247  oniso  28501  oldfib  28607  umgrres1lem  29697  upgrres1  29700  nbgrssvwo2  29749  ubthlem1  31259  issh2  31598  mdsymlem1  32792  iunxpssiun1  32950  padct  33100  xrofsup  33149  fz2ssnn0  33167  ccatws1f1o  33304  elrgspnlem1  33593  unitpidl1  33763  mxidlirred  33786  zarclsint  34293  tpr2rico  34333  sibfinima  34760  fct2relem  35015  bnj906  35349  bnj1014  35380  bnj1286  35438  bnj1408  35455  bnj1450  35469  bnj1452  35471  bnj1498  35480  bnj1501  35486  vonf1oonfo  35622  lfuhgr  35630  cvmopnlem  35790  cvmfolem  35791  cvmliftlem6  35802  cvmliftlem8  35804  cvmliftlem13  35808  cvmliftlem15  35810  cvmlift2lem9  35823  cvmlift2lem11  35825  cvmlift2lem12  35826  mclsppslem  36095  filnetlem4  36932  dissneqlem  38026  pibt2  38103  lindsdom  38305  opnmbllem0  38347  cnambfre  38359  heibor1lem  38500  osumcllem1N  40770  osumcllem2N  40771  pexmidlem6N  40789  dochexmidlem6  42279  dochexmidlem7  42280  mapdrvallem3  42460  evlsmhpvvval  43367  naddwordnexlem4  44168  k0004ss2  44918  cpcolld  45008  dvsconst  45080  dvsid  45081  dvsef  45082  iunconnlem2  45683  uzssd2  46171  climinf  46362  climsuse  46364  climresmpt  46413  climleltrp  46430  stoweidlem28  46782  stoweidlem50  46804  stoweidlem52  46806  stoweidlem53  46807  stoweidlem54  46808  fourierdlem54  46914  fourierdlem80  46940  meaiininclem  47240  caratheodorylem2  47281  hspmbllem2  47381  mbfresmf  47493  smfmbfcex  47514  smflimlem2  47526  smflimsuplem2  47575  smflimsuplem3  47576  smflimsuplem5  47578  smflimsuplem6  47579  gpgedgvtx1lem  48112  isuspgrim0  48699  gpgusgralem  48861  upgredgssspr  48948  setrec1  50509  setrecsres  50520  aacllem  50661