Theorem sseqtrrid 4036

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sseqtrrid.1	⊢ 𝐵 ⊆ 𝐴
sseqtrrid.2	⊢ (𝜑 → 𝐶 = 𝐴)

Assertion

Ref	Expression
sseqtrrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrrid

Step	Hyp	Ref	Expression
1		sseqtrrid.1	. 2 ⊢ 𝐵 ⊆ 𝐴
2		sseqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3	2	eqcomd 2737	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	1, 3	sseqtrid 4035	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3949

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  unissint  4977  resdif  6855  fimacnvOLD  7073  tfrlem5  8383  naddunif  8695  domss2  9139  dffi3  9429  cantnfp1lem3  9678  trcl  9726  tcid  9737  r1ordg  9776  r1sssuc  9781  ackbij1lem15  10232  cfsmolem  10268  fin1a2lem7  10404  wunex2  10736  wuncid  10741  trclfvlb  14960  rtrclreclem2  15011  fsumsplit  15692  o1fsum  15764  fprodsplit  15915  phimullem  16717  vdwlem6  16924  ressinbas  17195  mrcssid  17566  mreexexlem2d  17594  acsfiindd  18511  dirge  18561  symgbasfi  19288  efgredlemf  19651  efgredlemd  19654  gsumzres  19819  gsumzcl2  19820  gsumzf1o  19822  gsumadd  19833  gsumzsplit  19837  gsumsplit2  19839  dprd2da  19954  dmdprdsplit2lem  19957  dmdprdsplit2  19958  dmdprdsplit  19959  dprdsplit  19960  invrpropd  20310  issubdrg  20545  lspssid  20741  pjcss  21491  aspssid  21652  istopon  22635  sscls  22781  ordtbas  22917  cncls2  22998  tgcmp  23126  cmpfi  23133  1stcfb  23170  1stckgenlem  23278  ptbasfi  23306  ptcnplem  23346  ptuncnv  23532  ptunhmeo  23533  fbasrn  23609  cnflf2  23728  fclscmp  23755  alexsublem  23769  ghmcnp  23840  tsmsgsum  23864  tsmsres  23869  tsmssplit  23877  tsmsxplem1  23878  ustssco  23940  mopnfss  24170  cnmpopc  24670  uniiccdif  25328  uniioombllem3  25335  uniioombllem4  25336  itg2splitlem  25499  itg2split  25500  itgsplit  25586  ellimc2  25627  ellimc3  25629  lhop  25766  itgpowd  25800  plyaddlem1  25960  plymullem1  25961  taylthlem2  26119  mtest  26149  xrlimcnp  26706  fsumharmonic  26749  chtdif  26895  dchrghm  26992  lgsquadlem2  27117  dchrisumlema  27224  dchrisumlem2  27226  dchrisum0lem1b  27251  dchrisum0lem1  27252  pntrlog2bndlem6  27319  pntlemf  27341  precsexlem6  27894  precsexlem7  27895  sltonold  27923  nbupgruvtxres  28928  umgr2adedgwlk  29463  umgr2adedgwlkon  29464  umgr2adedgspth  29466  ex-res  29958  spanss2  30862  mdsymi  31928  padct  32208  cycpmco2lem5  32556  cycpmco2lem6  32557  cycpmco2lem7  32558  cycpmco2  32559  fldgenssid  32670  ordtconnlem1  33199  issgon  33416  sssigagen  33438  measiuns  33510  sitgclg  33636  cvmliftlem10  34580  satfsschain  34650  fmlasssuc  34675  satfun  34697  rdgssun  36563  ftc1anclem6  36870  heibor1lem  36981  heibor  36993  divrngcl  37129  isdrngo2  37130  igenss  37234  paddunssN  38983  sspadd1  38990  sspadd2  38991  pclssidN  39070  diassdvaN  40235  dochvalr  40532  lcdvbase  40768  nacsfix  41753  isnumbasgrplem2  42149  rgspnssid  42215  tfsconcatrnss12  42402  trrelsuperrel2dg  42725  fvilbd  42743  relexp0a  42770  wnefimgd  43216  grumnudlem  43347  icccncfext  44903  iblsplit  44982  dirkeritg  45118  dirkercncflem2  45120  fourierdlem81  45203  fourierdlem89  45211  fourierdlem91  45213  fourierdlem92  45214  fourierdlem111  45233  fouriercn  45248  hspdifhsp  45632  gsumsplit2f  46858  srhmsubc  47064  srhmsubcALTV  47082  fdivmpt  47315  fdivpm  47318  refdivpm  47319  mreclat  47711  elpglem2  47846