Theorem sseqtrid 3969

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.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		sseqtrid.1	. 2 ⊢ 𝐵 ⊆ 𝐴
3		sseq2 3943	. . 3 ⊢ (𝐴 = 𝐶 → (𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐶))
4	3	biimpa 476	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐶)
5	1, 2, 4	sylancl 585	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  iunxdif3  5020  fssdm  6604  fndmdif  6901  fneqeql2  6906  fconst4  7072  isofrlem  7191  f1opw2  7502  fparlem3  7925  fparlem4  7926  fnwelem  7943  frnsuppeq  7962  frnsuppeqg  7963  ecss  8502  pw2f1olem  8816  fopwdom  8820  ssenen  8887  phplem2  8893  ssfiALT  8919  fiint  9021  f1opwfi  9053  kmlem5  9841  enfin2i  10008  fpwwe2lem5  10322  fpwwe2lem8  10325  tskuni  10470  monoord2  13682  seqz  13699  cshimadifsn0  14471  binom1dif  15473  bpolycl  15690  bpolysum  15691  bpolydiflem  15692  bitsres  16108  prdshom  17095  imasless  17168  cntzval  18842  f1omvdmvd  18966  f1omvdconj  18969  pmtrfb  18988  symggen  18993  symggen2  18994  psgnunilem1  19016  gsumzaddlem  19437  isdrngd  19931  lspextmo  20233  znleval  20674  ordtcld1  22256  ordtcld2  22257  cnpnei  22323  cnntri  22330  cncls2  22332  cncls  22333  cnntr  22334  cncnp  22339  cndis  22350  paste  22353  cmpfi  22467  conncompcld  22493  1stcfb  22504  1stccnp  22521  cldllycmp  22554  llycmpkgen2  22609  kgencn  22615  kgencn3  22617  dfac14lem  22676  txdis1cn  22694  hausdiag  22704  txkgen  22711  qtopval2  22755  basqtop  22770  qtopcld  22772  qtopeu  22775  qtoprest  22776  imastopn  22779  hmeontr  22828  hmeoimaf1o  22829  cmphaushmeo  22859  ordthmeolem  22860  elfm3  23009  rnelfmlem  23011  rnelfm  23012  alexsubALTlem4  23109  cldsubg  23170  tgpconncompeqg  23171  tgpconncomp  23172  qustgpopn  23179  qustgplem  23180  tsmsf1o  23204  ucncn  23345  imasf1oxms  23551  blcld  23567  metustfbas  23619  cfilucfil  23621  metuel2  23627  icchmeo  24010  relcmpcmet  24387  minveclem4a  24499  nulmbl2  24605  icombl  24633  ioombl  24634  uniiccdif  24647  volivth  24676  mbfres2  24714  itg1addlem5  24770  itgsplitioo  24907  dvcobr  25015  dvcnvlem  25045  lhop1lem  25082  lhop  25085  dvcnvrelem2  25087  uc1pval  25209  mon1pval  25211  vieta1lem2  25376  basellem5  26139  f1otrg  27136  axlowdimlem13  27225  axcontlem10  27244  uhgrspansubgr  27561  vtxdun  27751  pthdlem1  28035  eucrct2eupth  28510  ssmd1  30574  mdslj2i  30583  atcvat4i  30660  imadifxp  30841  nfpconfp  30868  2ndresdju  30887  ofpreima  30904  ofpreima2  30905  fsuppcurry1  30962  fsuppcurry2  30963  gsumpart  31217  symgcom  31254  symgcom2  31255  pmtrcnel  31260  cycpmfvlem  31281  cycpmfv3  31284  freshmansdream  31386  elrspunidl  31508  idlinsubrg  31510  qtophaus  31688  reff  31691  locfinreflem  31692  zarcmplem  31733  hauseqcn  31750  indpreima  31893  indf1ofs  31894  oms0  32164  eulerpartlemv  32231  eulerpartlemb  32235  eulerpartlemr  32241  eulerpartlemgs2  32247  eulerpartlemn  32248  ballotlemro  32389  bnj1253  32897  bnj1280  32900  pthhashvtx  32989  acycgr0v  33010  prclisacycgr  33013  subfacp1lem3  33044  cvmscld  33135  cvmsss2  33136  cvmliftmolem1  33143  cvmliftlem7  33153  cvmlift2lem9  33173  cvmlift3lem7  33187  fnessref  34473  tailf  34491  poimirlem3  35707  mbfresfi  35750  cnambfre  35752  itg2addnclem2  35756  mettrifi  35842  ismtyres  35893  isdrngo2  36043  diaintclN  38999  dibintclN  39108  dihintcl  39285  dochocss  39307  mapdunirnN  39591  pw2f1ocnv  40775  wessf1ornlem  42611  monoord2xrv  42914  itgcoscmulx  43400  ibliooicc  43402  stoweidlem11  43442  stoweidlem34  43465  fourierdlem48  43585  fourierdlem49  43586  fourierdlem74  43611  uniimaprimaeqfv  44722  elsetpreimafvssdm  44726  rngcbas  45411  ringcbas  45457  fdivmptf  45775  refdivmptf  45776  iscnrm3llem2  46132