Theorem sseqtrrid 3981

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  unissint  4925  resdif  6789  tfrlem5  8309  naddunif  8618  domss2  9060  dffi3  9340  cantnfp1lem3  9595  trcl  9643  tcid  9654  r1ordg  9693  r1sssuc  9698  ackbij1lem15  10146  cfsmolem  10183  fin1a2lem7  10319  wunex2  10651  wuncid  10656  trclfvlb  14933  rtrclreclem2  14984  fsumsplit  15666  o1fsum  15738  fprodsplit  15891  phimullem  16708  vdwlem6  16916  ressinbas  17174  mrcssid  17541  mreexexlem2d  17569  acsfiindd  18477  dirge  18527  symgbasfi  19276  efgredlemf  19638  efgredlemd  19641  gsumzres  19806  gsumzcl2  19807  gsumzf1o  19809  gsumadd  19820  gsumzsplit  19824  gsumsplit2  19826  dprd2da  19941  dmdprdsplit2lem  19944  dmdprdsplit2  19945  dmdprdsplit  19946  dprdsplit  19947  invrpropd  20321  rgspnssid  20517  srhmsubc  20583  issubdrg  20683  lspssid  20906  pjcss  21641  aspssid  21803  psdmul  22069  istopon  22815  sscls  22959  ordtbas  23095  cncls2  23176  tgcmp  23304  cmpfi  23311  1stcfb  23348  1stckgenlem  23456  ptbasfi  23484  ptcnplem  23524  ptuncnv  23710  ptunhmeo  23711  fbasrn  23787  cnflf2  23906  fclscmp  23933  alexsublem  23947  ghmcnp  24018  tsmsgsum  24042  tsmsres  24047  tsmssplit  24055  tsmsxplem1  24056  ustssco  24118  mopnfss  24347  cnmpopc  24838  uniiccdif  25495  uniioombllem3  25502  uniioombllem4  25503  itg2splitlem  25665  itg2split  25666  itgsplit  25753  ellimc2  25794  ellimc3  25796  lhop  25937  itgpowd  25973  plyaddlem1  26134  plymullem1  26135  taylthlem2  26298  taylthlem2OLD  26299  mtest  26329  xrlimcnp  26894  fsumharmonic  26938  chtdif  27084  dchrghm  27183  lgsquadlem2  27308  dchrisumlema  27415  dchrisumlem2  27417  dchrisum0lem1b  27442  dchrisum0lem1  27443  pntrlog2bndlem6  27510  pntlemf  27532  precsexlem6  28137  precsexlem7  28138  sltonold  28185  nbupgruvtxres  29370  cyclnumvtx  29763  umgr2adedgwlk  29908  umgr2adedgwlkon  29909  umgr2adedgspth  29911  ex-res  30403  spanss2  31307  mdsymi  32373  padct  32676  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmco2  33088  fldgenssid  33262  ordtconnlem1  33890  issgon  34089  sssigagen  34111  measiuns  34183  sitgclg  34309  cvmliftlem10  35266  satfsschain  35336  fmlasssuc  35361  satfun  35383  rdgssun  37351  ftc1anclem6  37677  heibor1lem  37788  heibor  37800  divrngcl  37936  isdrngo2  37937  igenss  38041  paddunssN  39787  sspadd1  39794  sspadd2  39795  pclssidN  39874  diassdvaN  41039  dochvalr  41336  lcdvbase  41572  nacsfix  42685  isnumbasgrplem2  43077  tfsconcatrnss12  43322  trrelsuperrel2dg  43644  fvilbd  43662  relexp0a  43689  wnefimgd  44134  grumnudlem  44258  icccncfext  45869  iblsplit  45948  dirkeritg  46084  dirkercncflem2  46086  fourierdlem81  46169  fourierdlem89  46177  fourierdlem91  46179  fourierdlem92  46180  fourierdlem111  46199  fouriercn  46214  hspdifhsp  46598  3f1oss1  47060  dfnbgrss  47837  dfnbgrss2  47844  gsumsplit2f  48165  srhmsubcALTV  48310  fdivmpt  48526  fdivpm  48529  refdivpm  48530  mreclat  48982  elpglem2  49698