Theorem sseqtrrdi 3954

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3sstr4g  3966  abssdv  3995  disjxiun  5103  knatar  7390  iunpw  7809  fviunfun  7981  frrlem8  8339  frrlem10  8341  frrlem12  8343  frrlem14  8345  fprresex  8356  tfrlem9  8421  tfrlem9a  8422  tfrlem13  8426  tz7.44-2  8443  tz7.44-3  8444  tz7.49  8483  naddcllem  8713  naddov2  8716  naddasslem1  8732  naddasslem2  8733  marypha1lem  9452  ordtypelem2  9540  ixpiunwdom  9611  oemapvali  9712  tcss  9770  tcel  9771  pwwf  9842  rankpwi  9859  rankval3b  9863  cplem1  9977  cplem1OLD  9978  setrec1  9999  dfac12lem2  10250  infmap2  10322  ackbij1b  10343  ttukeylem6  10619  fpwwe2lem10  10752  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  uznnssnn  13049  pfxccatpfx2  14914  shftfval  15252  rexuzre  15549  climsup  15866  clim2prod  16086  fprodntriv  16138  eulerthlem2  16988  ramtlecl  17207  mreexexlem4d  17850  mreexdomd  17852  gsumpropd2lem  18897  gsumzaddlem  20165  gsum2d  20216  telgsums  20237  pgpfac1lem1  20320  pgpfac1lem3a  20322  pgpfac1lem3  20323  pgpfac1lem5  20325  lspsolvlem  21450  lbsextlem2  21467  dsmmacl  22077  lindsdom  22186  eltopss  23255  difopn  23382  tgrest  23507  perfopn  23533  pnfnei  23568  mnfnei  23569  regsep2  23724  cncmp  23740  uncmp  23751  hauscmplem  23754  hauscmp  23755  conndisj  23764  cnconn  23770  conncompss  23781  2ndcctbss  23804  islly2  23833  comppfsc  23881  1stckgenlem  23902  txuni2  23914  ptbasfi  23930  ptpjopn  23961  txindis  23983  txtube  23989  hausdiag  23994  xkoinjcn  24036  tgqtop  24061  filconn  24232  elfm2  24297  flimclslem  24333  flffbas  24344  fclsbas  24370  flimfnfcls  24377  alexsubALT  24400  symgtgp  24455  ustssco  24564  isucn2  24627  ucnima  24629  ucnprima  24630  blcls  24855  prdsxmslem2  24878  isngp2  24946  tgioo  25145  xrtgioo  25156  xrsmopn  25162  opnreen  25181  cnheiborlem  25305  cnllycmp  25307  tcphcph  25588  rrxmvallem  25755  uniioombllem4  25937  dyadmbllem  25950  opnmbllem  25952  mbfimaopnlem  26006  mbflimsup  26017  i1fadd  26046  i1fmul  26047  itg1addlem4  26050  i1fmulc  26054  limciun  26244  dvlip2  26345  c1lip3  26349  lhop  26366  dvfsumlem2  26377  dvfsumrlimge0  26380  dvfsumrlim2  26382  ulmval  26737  psercnlem2  26781  efopnlem2  27015  efopn  27016  madebdayim  28304  madefi  28329  oldfi  28330  addbdaylem  28433  oniso  28687  oldfib  28793  lfuhgr  29756  umgrres1lem  29921  upgrres1  29924  nbgrssvwo2  29973  ubthlem1  31502  issh2  31841  mdsymlem1  33035  iunxpssiun1  33234  padct  33381  xrofsup  33429  fz2ssnn0  33447  ccatws1f1o  33584  elrgspnlem1  33873  unitpidl1  34044  mxidlirred  34067  zarclsint  34574  tpr2rico  34614  sibfinima  35041  fct2relem  35296  bnj906  35630  bnj1014  35661  bnj1286  35719  bnj1408  35736  bnj1450  35750  bnj1452  35752  bnj1498  35761  bnj1501  35767  vonf1oonfo  36049  cvmopnlem  36210  cvmfolem  36211  cvmliftlem6  36222  cvmliftlem8  36224  cvmliftlem13  36228  cvmliftlem15  36230  cvmlift2lem9  36243  cvmlift2lem11  36245  cvmlift2lem12  36246  mclsppslem  36515  filnetlem4  37347  dissneqlem  38455  pibt2  38532  opnmbllem0  38766  cnambfre  38778  heibor1lem  38935  osumcllem1N  41205  osumcllem2N  41206  pexmidlem6N  41224  dochexmidlem6  42714  dochexmidlem7  42715  mapdrvallem3  42895  evlsmhpvvval  43816  naddwordnexlem4  44595  k0004ss2  45344  cpcolld  45434  dvsconst  45506  dvsid  45507  dvsef  45508  iunconnlem2  46108  hfstructcan  46229  uzssd2  46632  climinf  46823  climsuse  46825  climresmpt  46874  climleltrp  46891  stoweidlem28  47243  stoweidlem50  47265  stoweidlem52  47267  stoweidlem53  47268  stoweidlem54  47269  fourierdlem54  47375  fourierdlem80  47401  meaiininclem  47701  caratheodorylem2  47742  hspmbllem2  47842  mbfresmf  47954  smfmbfcex  47975  smflimlem2  47987  smflimsuplem2  48036  smflimsuplem3  48037  smflimsuplem5  48039  smflimsuplem6  48040  gpgedgvtx1lem  48610  isuspgrim0  49197  gpgusgralem  49359  upgredgssspr  49446  setrecsres  51075  aacllem  51219