Theorem sseqtrid 4034

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

Hypotheses

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

Assertion

Ref	Expression
sseqtrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrid

Step	Hyp	Ref	Expression
1		sseqtrid.1	. . 3 ⊢ 𝐵 ⊆ 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		sseqtrid.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	sseqtrd 4022	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

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

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 3955  df-ss 3965

This theorem is referenced by:  sseqtrrid  4035  iunxdif3  5098  fssdm  6737  fndmdif  7043  fneqeql2  7048  fconst4  7218  isofrlem  7340  fvmptopab  7466  f1opw2  7665  fparlem3  8105  fparlem4  8106  fnwelem  8122  fsuppeq  8165  fsuppeqg  8166  ecss  8755  pw2f1olem  9082  fopwdom  9086  ssenen  9157  ssfiALT  9180  phplem2OLD  9224  fiint  9330  f1opwfi  9362  kmlem5  10155  enfin2i  10322  fpwwe2lem5  10636  fpwwe2lem8  10639  tskuni  10784  monoord2  14006  seqz  14023  cshimadifsn0  14788  binom1dif  15786  bpolycl  16003  bpolysum  16004  bpolydiflem  16005  bitsres  16421  prdshom  17420  imasless  17493  cntzval  19230  f1omvdmvd  19356  f1omvdconj  19359  pmtrfb  19378  symggen  19383  symggen2  19384  psgnunilem1  19406  gsumzaddlem  19834  isdrngd  20537  isdrngdOLD  20539  lspextmo  20815  znleval  21333  ordtcld1  22934  ordtcld2  22935  cnpnei  23001  cnntri  23008  cncls2  23010  cncls  23011  cnntr  23012  cncnp  23017  cndis  23028  paste  23031  cmpfi  23145  conncompcld  23171  1stcfb  23182  1stccnp  23199  cldllycmp  23232  llycmpkgen2  23287  kgencn  23293  kgencn3  23295  dfac14lem  23354  txdis1cn  23372  hausdiag  23382  txkgen  23389  qtopval2  23433  basqtop  23448  qtopcld  23450  qtopeu  23453  qtoprest  23454  imastopn  23457  hmeontr  23506  hmeoimaf1o  23507  cmphaushmeo  23537  ordthmeolem  23538  elfm3  23687  rnelfmlem  23689  rnelfm  23690  alexsubALTlem4  23787  cldsubg  23848  tgpconncompeqg  23849  tgpconncomp  23850  qustgpopn  23857  qustgplem  23858  tsmsf1o  23882  ucncn  24023  imasf1oxms  24231  blcld  24247  metustfbas  24299  cfilucfil  24301  metuel2  24307  icchmeo  24698  icchmeoOLD  24699  relcmpcmet  25079  minveclem4a  25191  nulmbl2  25298  icombl  25326  ioombl  25327  uniiccdif  25340  volivth  25369  mbfres2  25407  itg1addlem5  25463  itgsplitioo  25600  dvcobr  25710  dvcobrOLD  25711  dvcnvlem  25741  lhop1lem  25779  lhop  25782  dvcnvrelem2  25784  uc1pval  25906  mon1pval  25908  vieta1lem2  26074  basellem5  26840  f1otrg  28404  axlowdimlem13  28494  axcontlem10  28513  uhgrspansubgr  28830  vtxdun  29020  pthdlem1  29305  eucrct2eupth  29780  ssmd1  31846  mdslj2i  31855  atcvat4i  31932  imadifxp  32114  nfpconfp  32138  2ndresdju  32156  ofpreima  32172  ofpreima2  32173  fsuppcurry1  32232  fsuppcurry2  32233  gsumpart  32492  symgcom  32529  symgcom2  32530  pmtrcnel  32535  cycpmfvlem  32556  cycpmfv3  32559  freshmansdream  32666  elrspunidl  32835  idlinsubrg  32838  qtophaus  33129  reff  33132  locfinreflem  33133  zarcmplem  33174  hauseqcn  33191  indpreima  33336  indf1ofs  33337  oms0  33609  eulerpartlemv  33676  eulerpartlemb  33680  eulerpartlemr  33686  eulerpartlemgs2  33692  eulerpartlemn  33693  ballotlemro  33834  bnj1253  34341  bnj1280  34344  pthhashvtx  34431  acycgr0v  34452  prclisacycgr  34455  subfacp1lem3  34486  cvmscld  34577  cvmsss2  34578  cvmliftmolem1  34585  cvmliftlem7  34595  cvmlift2lem9  34615  cvmlift3lem7  34629  fnessref  35558  tailf  35576  poimirlem3  36807  mbfresfi  36850  cnambfre  36852  itg2addnclem2  36856  mettrifi  36941  ismtyres  36992  isdrngo2  37142  diaintclN  40245  dibintclN  40354  dihintcl  40531  dochocss  40553  mapdunirnN  40837  pw2f1ocnv  42091  wessf1ornlem  44195  monoord2xrv  44505  itgcoscmulx  44996  ibliooicc  44998  stoweidlem11  45038  stoweidlem34  45061  fourierdlem48  45181  fourierdlem49  45182  fourierdlem74  45207  uniimaprimaeqfv  46361  elsetpreimafvssdm  46365  rngcbas  46964  ringcbas  47010  fdivmptf  47327  refdivmptf  47328  iscnrm3llem2  47683