Theorem sseqtrrid 3965

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  unissint  4914  resdif  6801  tfrlem5  8319  naddunif  8629  domss2  9074  dffi3  9344  cantnfp1lem3  9601  trcl  9649  tcid  9658  r1ordg  9702  r1sssuc  9707  ackbij1lem15  10155  cfsmolem  10192  fin1a2lem7  10328  wunex2  10661  wuncid  10666  trclfvlb  14970  rtrclreclem2  15021  fsumsplit  15703  o1fsum  15776  fprodsplit  15931  phimullem  16749  vdwlem6  16957  ressinbas  17215  mrcssid  17583  mreexexlem2d  17611  acsfiindd  18519  dirge  18569  symgbasfi  19354  efgredlemf  19716  efgredlemd  19719  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumadd  19898  gsumzsplit  19902  gsumsplit2  19904  dprd2da  20019  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dmdprdsplit  20024  dprdsplit  20025  invrpropd  20398  rgspnssid  20591  srhmsubc  20657  issubdrg  20757  lspssid  20980  pjcss  21696  aspssid  21857  psdmul  22132  istopon  22877  sscls  23021  ordtbas  23157  cncls2  23238  tgcmp  23366  cmpfi  23373  1stcfb  23410  1stckgenlem  23518  ptbasfi  23546  ptcnplem  23586  ptuncnv  23772  ptunhmeo  23773  fbasrn  23849  cnflf2  23968  fclscmp  23995  alexsublem  24009  ghmcnp  24080  tsmsgsum  24104  tsmsres  24109  tsmssplit  24117  tsmsxplem1  24118  ustssco  24180  mopnfss  24408  cnmpopc  24895  uniiccdif  25545  uniioombllem3  25552  uniioombllem4  25553  itg2splitlem  25715  itg2split  25716  itgsplit  25803  ellimc2  25844  ellimc3  25846  lhop  25983  itgpowd  26017  plyaddlem1  26178  plymullem1  26179  taylthlem2  26339  mtest  26369  xrlimcnp  26932  fsumharmonic  26975  chtdif  27121  dchrghm  27219  lgsquadlem2  27344  dchrisumlema  27451  dchrisumlem2  27453  dchrisum0lem1b  27478  dchrisum0lem1  27479  pntrlog2bndlem6  27546  pntlemf  27568  precsexlem6  28204  precsexlem7  28205  ltonold  28253  nbupgruvtxres  29476  cyclnumvtx  29868  umgr2adedgwlk  30013  umgr2adedgwlkon  30014  umgr2adedgspth  30016  ex-res  30511  spanss2  31416  mdsymi  32482  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  fldgenssid  33374  vietalem  33723  ordtconnlem1  34068  issgon  34267  sssigagen  34289  measiuns  34361  sitgclg  34486  cvmliftlem10  35476  satfsschain  35546  fmlasssuc  35571  satfun  35593  dfttc3gw  36705  rdgssun  37694  ftc1anclem6  38019  heibor1lem  38130  heibor  38142  divrngcl  38278  isdrngo2  38279  igenss  38383  paddunssN  40254  sspadd1  40261  sspadd2  40262  pclssidN  40341  diassdvaN  41506  dochvalr  41803  lcdvbase  42039  nacsfix  43144  isnumbasgrplem2  43532  tfsconcatrnss12  43777  trrelsuperrel2dg  44098  fvilbd  44116  relexp0a  44143  wnefimgd  44588  grumnudlem  44712  icccncfext  46315  iblsplit  46394  dirkeritg  46530  dirkercncflem2  46532  fourierdlem81  46615  fourierdlem89  46623  fourierdlem91  46625  fourierdlem92  46626  fourierdlem111  46645  fouriercn  46660  hspdifhsp  47044  3f1oss1  47523  dfnbgrss  48328  dfnbgrss2  48335  gsumsplit2f  48656  srhmsubcALTV  48801  fdivmpt  49016  fdivpm  49019  refdivpm  49020  mreclat  49472  elpglem2  50187