Theorem sseqtrid 4033

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 4021	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  sseqtrrid  4034  iunxdif3  5097  fssdm  6736  fndmdif  7042  fneqeql2  7047  fconst4  7217  isofrlem  7339  fvmptopab  7465  f1opw2  7663  fparlem3  8102  fparlem4  8103  fnwelem  8119  fsuppeq  8162  fsuppeqg  8163  ecss  8751  pw2f1olem  9078  fopwdom  9082  ssenen  9153  ssfiALT  9176  phplem2OLD  9220  fiint  9326  f1opwfi  9358  kmlem5  10151  enfin2i  10318  fpwwe2lem5  10632  fpwwe2lem8  10635  tskuni  10780  monoord2  14003  seqz  14020  cshimadifsn0  14785  binom1dif  15783  bpolycl  16000  bpolysum  16001  bpolydiflem  16002  bitsres  16418  prdshom  17417  imasless  17490  cntzval  19226  f1omvdmvd  19352  f1omvdconj  19355  pmtrfb  19374  symggen  19379  symggen2  19380  psgnunilem1  19402  gsumzaddlem  19830  isdrngd  20533  isdrngdOLD  20535  lspextmo  20811  znleval  21329  ordtcld1  22921  ordtcld2  22922  cnpnei  22988  cnntri  22995  cncls2  22997  cncls  22998  cnntr  22999  cncnp  23004  cndis  23015  paste  23018  cmpfi  23132  conncompcld  23158  1stcfb  23169  1stccnp  23186  cldllycmp  23219  llycmpkgen2  23274  kgencn  23280  kgencn3  23282  dfac14lem  23341  txdis1cn  23359  hausdiag  23369  txkgen  23376  qtopval2  23420  basqtop  23435  qtopcld  23437  qtopeu  23440  qtoprest  23441  imastopn  23444  hmeontr  23493  hmeoimaf1o  23494  cmphaushmeo  23524  ordthmeolem  23525  elfm3  23674  rnelfmlem  23676  rnelfm  23677  alexsubALTlem4  23774  cldsubg  23835  tgpconncompeqg  23836  tgpconncomp  23837  qustgpopn  23844  qustgplem  23845  tsmsf1o  23869  ucncn  24010  imasf1oxms  24218  blcld  24234  metustfbas  24286  cfilucfil  24288  metuel2  24294  icchmeo  24685  icchmeoOLD  24686  relcmpcmet  25066  minveclem4a  25178  nulmbl2  25285  icombl  25313  ioombl  25314  uniiccdif  25327  volivth  25356  mbfres2  25394  itg1addlem5  25450  itgsplitioo  25587  dvcobr  25697  dvcobrOLD  25698  dvcnvlem  25728  lhop1lem  25765  lhop  25768  dvcnvrelem2  25770  uc1pval  25892  mon1pval  25894  vieta1lem2  26060  basellem5  26825  f1otrg  28389  axlowdimlem13  28479  axcontlem10  28498  uhgrspansubgr  28815  vtxdun  29005  pthdlem1  29290  eucrct2eupth  29765  ssmd1  31831  mdslj2i  31840  atcvat4i  31917  imadifxp  32099  nfpconfp  32123  2ndresdju  32141  ofpreima  32157  ofpreima2  32158  fsuppcurry1  32217  fsuppcurry2  32218  gsumpart  32477  symgcom  32514  symgcom2  32515  pmtrcnel  32520  cycpmfvlem  32541  cycpmfv3  32544  freshmansdream  32651  elrspunidl  32820  idlinsubrg  32823  qtophaus  33114  reff  33117  locfinreflem  33118  zarcmplem  33159  hauseqcn  33176  indpreima  33321  indf1ofs  33322  oms0  33594  eulerpartlemv  33661  eulerpartlemb  33665  eulerpartlemr  33671  eulerpartlemgs2  33677  eulerpartlemn  33678  ballotlemro  33819  bnj1253  34326  bnj1280  34329  pthhashvtx  34416  acycgr0v  34437  prclisacycgr  34440  subfacp1lem3  34471  cvmscld  34562  cvmsss2  34563  cvmliftmolem1  34570  cvmliftlem7  34580  cvmlift2lem9  34600  cvmlift3lem7  34614  fnessref  35545  tailf  35563  poimirlem3  36794  mbfresfi  36837  cnambfre  36839  itg2addnclem2  36843  mettrifi  36928  ismtyres  36979  isdrngo2  37129  diaintclN  40232  dibintclN  40341  dihintcl  40518  dochocss  40540  mapdunirnN  40824  pw2f1ocnv  42078  wessf1ornlem  44182  monoord2xrv  44492  itgcoscmulx  44983  ibliooicc  44985  stoweidlem11  45025  stoweidlem34  45048  fourierdlem48  45168  fourierdlem49  45169  fourierdlem74  45194  uniimaprimaeqfv  46348  elsetpreimafvssdm  46352  rngcbas  46951  ringcbas  46997  fdivmptf  47314  refdivmptf  47315  iscnrm3llem2  47670