Theorem sseqtrrdi 3949

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  3sstr4g  3961  abssdv  3992  disjxiun  5099  knatar  7367  iunpw  7785  fviunfun  7957  frrlem8  8314  frrlem10  8316  frrlem12  8318  frrlem14  8320  fprresex  8331  tfrlem9  8396  tfrlem9a  8397  tfrlem13  8401  tz7.44-2  8418  tz7.44-3  8419  tz7.49  8458  naddcllem  8688  naddov2  8691  naddasslem1  8707  naddasslem2  8708  marypha1lem  9428  ordtypelem2  9516  ixpiunwdom  9587  oemapvali  9688  tcss  9746  tcel  9747  pwwf  9818  rankpwi  9835  rankval3b  9839  cplem1  9953  cplem1OLD  9954  setrec1  9975  dfac12lem2  10226  infmap2  10298  ackbij1b  10319  ttukeylem6  10595  fpwwe2lem10  10728  fpwwe2lem11  10729  fpwwe2lem12  10730  fpwwe2  10731  uznnssnn  13025  pfxccatpfx2  14890  shftfval  15228  rexuzre  15525  climsup  15842  clim2prod  16062  fprodntriv  16114  eulerthlem2  16964  ramtlecl  17183  mreexexlem4d  17826  mreexdomd  17828  gsumpropd2lem  18873  gsumzaddlem  20140  gsum2d  20191  telgsums  20212  pgpfac1lem1  20295  pgpfac1lem3a  20297  pgpfac1lem3  20298  pgpfac1lem5  20300  lspsolvlem  21425  lbsextlem2  21442  dsmmacl  22052  lindsdom  22161  eltopss  23230  difopn  23357  tgrest  23482  perfopn  23508  pnfnei  23543  mnfnei  23544  regsep2  23699  cncmp  23715  uncmp  23726  hauscmplem  23729  hauscmp  23730  conndisj  23739  cnconn  23745  conncompss  23756  2ndcctbss  23779  islly2  23808  comppfsc  23856  1stckgenlem  23877  txuni2  23889  ptbasfi  23905  ptpjopn  23936  txindis  23958  txtube  23964  hausdiag  23969  xkoinjcn  24011  tgqtop  24036  filconn  24207  elfm2  24272  flimclslem  24308  flffbas  24319  fclsbas  24345  flimfnfcls  24352  alexsubALT  24375  symgtgp  24430  ustssco  24539  isucn2  24602  ucnima  24604  ucnprima  24605  blcls  24830  prdsxmslem2  24853  isngp2  24921  tgioo  25120  xrtgioo  25131  xrsmopn  25137  opnreen  25156  cnheiborlem  25280  cnllycmp  25282  tcphcph  25563  rrxmvallem  25730  uniioombllem4  25912  dyadmbllem  25925  opnmbllem  25927  mbfimaopnlem  25981  mbflimsup  25992  i1fadd  26021  i1fmul  26022  itg1addlem4  26025  i1fmulc  26029  limciun  26219  dvlip2  26320  c1lip3  26324  lhop  26341  dvfsumlem2  26352  dvfsumrlimge0  26355  dvfsumrlim2  26357  ulmval  26712  psercnlem2  26756  efopnlem2  26990  efopn  26991  madebdayim  28279  madefi  28304  oldfi  28305  addbdaylem  28408  oniso  28662  oldfib  28768  lfuhgr  29731  umgrres1lem  29896  upgrres1  29899  nbgrssvwo2  29948  ubthlem1  31477  issh2  31816  mdsymlem1  33010  iunxpssiun1  33209  padct  33357  xrofsup  33405  fz2ssnn0  33423  ccatws1f1o  33560  elrgspnlem1  33849  unitpidl1  34020  mxidlirred  34043  zarclsint  34550  tpr2rico  34590  sibfinima  35017  fct2relem  35272  bnj906  35606  bnj1014  35637  bnj1286  35695  bnj1408  35712  bnj1450  35726  bnj1452  35728  bnj1498  35737  bnj1501  35743  vonf1oonfo  35968  cvmopnlem  36129  cvmfolem  36130  cvmliftlem6  36141  cvmliftlem8  36143  cvmliftlem13  36147  cvmliftlem15  36149  cvmlift2lem9  36162  cvmlift2lem11  36164  cvmlift2lem12  36165  mclsppslem  36434  filnetlem4  37261  dissneqlem  38356  pibt2  38433  opnmbllem0  38667  cnambfre  38679  heibor1lem  38836  osumcllem1N  41106  osumcllem2N  41107  pexmidlem6N  41125  dochexmidlem6  42615  dochexmidlem7  42616  mapdrvallem3  42796  evlsmhpvvval  43716  naddwordnexlem4  44496  k0004ss2  45245  cpcolld  45335  dvsconst  45407  dvsid  45408  dvsef  45409  iunconnlem2  46010  hfstructcan  46124  uzssd2  46520  climinf  46711  climsuse  46713  climresmpt  46762  climleltrp  46779  stoweidlem28  47131  stoweidlem50  47153  stoweidlem52  47155  stoweidlem53  47156  stoweidlem54  47157  fourierdlem54  47263  fourierdlem80  47289  meaiininclem  47589  caratheodorylem2  47630  hspmbllem2  47730  mbfresmf  47842  smfmbfcex  47863  smflimlem2  47875  smflimsuplem2  47924  smflimsuplem3  47925  smflimsuplem5  47927  smflimsuplem6  47928  gpgedgvtx1lem  48498  isuspgrim0  49085  gpgusgralem  49247  upgredgssspr  49334  setrecsres  50963  aacllem  51107