Theorem sseqtrid 3967

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 3941	. . 3 ⊢ (𝐴 = 𝐶 → (𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐶))
4	3	biimpa 480	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐶)
5	1, 2, 4	sylancl 589	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  iunxdif3  4980  fssdm  6504  fndmdif  6789  fneqeql2  6794  fconst4  6954  isofrlem  7072  f1opw2  7380  fparlem3  7792  fparlem4  7793  fnwelem  7808  frnsuppeq  7825  ecss  8318  pw2f1olem  8604  fopwdom  8608  ssenen  8675  phplem2  8681  ssfi  8722  fiint  8779  f1opwfi  8812  kmlem5  9565  enfin2i  9732  fpwwe2lem6  10046  fpwwe2lem9  10049  tskuni  10194  monoord2  13397  seqz  13414  cshimadifsn0  14183  binom1dif  15180  bpolycl  15398  bpolysum  15399  bpolydiflem  15400  bitsres  15812  prdshom  16732  imasless  16805  cntzval  18443  f1omvdmvd  18563  f1omvdconj  18566  pmtrfb  18585  symggen  18590  symggen2  18591  psgnunilem1  18613  gsumzaddlem  19034  isdrngd  19520  lspextmo  19821  znleval  20246  ordtcld1  21802  ordtcld2  21803  cnpnei  21869  cnntri  21876  cncls2  21878  cncls  21879  cnntr  21880  cncnp  21885  cndis  21896  paste  21899  cmpfi  22013  conncompcld  22039  1stcfb  22050  1stccnp  22067  cldllycmp  22100  llycmpkgen2  22155  kgencn  22161  kgencn3  22163  dfac14lem  22222  txdis1cn  22240  hausdiag  22250  txkgen  22257  qtopval2  22301  basqtop  22316  qtopcld  22318  qtopeu  22321  qtoprest  22322  imastopn  22325  hmeontr  22374  hmeoimaf1o  22375  cmphaushmeo  22405  ordthmeolem  22406  elfm3  22555  rnelfmlem  22557  rnelfm  22558  alexsubALTlem4  22655  cldsubg  22716  tgpconncompeqg  22717  tgpconncomp  22718  qustgpopn  22725  qustgplem  22726  tsmsf1o  22750  ucncn  22891  imasf1oxms  23096  blcld  23112  metustfbas  23164  cfilucfil  23166  metuel2  23172  icchmeo  23546  relcmpcmet  23922  minveclem4a  24034  nulmbl2  24140  icombl  24168  ioombl  24169  uniiccdif  24182  volivth  24211  mbfres2  24249  itg1addlem5  24304  itgsplitioo  24441  dvcobr  24549  dvcnvlem  24579  lhop1lem  24616  lhop  24619  dvcnvrelem2  24621  uc1pval  24740  mon1pval  24742  vieta1lem2  24907  basellem5  25670  f1otrg  26665  axlowdimlem13  26748  axcontlem10  26767  uhgrspansubgr  27081  vtxdun  27271  pthdlem1  27555  eucrct2eupth  28030  ssmd1  30094  mdslj2i  30103  atcvat4i  30180  imadifxp  30364  nfpconfp  30391  2ndresdju  30411  ofpreima  30428  ofpreima2  30429  fsuppcurry1  30487  fsuppcurry2  30488  gsumpart  30740  symgcom  30777  symgcom2  30778  pmtrcnel  30783  cycpmfvlem  30804  cycpmfv3  30807  freshmansdream  30909  elrspunidl  31014  idlinsubrg  31016  qtophaus  31189  reff  31192  locfinreflem  31193  zarcmplem  31234  hauseqcn  31251  indpreima  31394  indf1ofs  31395  oms0  31665  eulerpartlemv  31732  eulerpartlemb  31736  eulerpartlemr  31742  eulerpartlemgs2  31748  eulerpartlemn  31749  ballotlemro  31890  bnj1253  32399  bnj1280  32402  pthhashvtx  32487  acycgr0v  32508  prclisacycgr  32511  subfacp1lem3  32542  cvmscld  32633  cvmsss2  32634  cvmliftmolem1  32641  cvmliftlem7  32651  cvmlift2lem9  32671  cvmlift3lem7  32685  fnessref  33818  tailf  33836  poimirlem3  35060  mbfresfi  35103  cnambfre  35105  itg2addnclem2  35109  mettrifi  35195  ismtyres  35246  isdrngo2  35396  diaintclN  38354  dibintclN  38463  dihintcl  38640  dochocss  38662  mapdunirnN  38946  pw2f1ocnv  39978  wessf1ornlem  41811  monoord2xrv  42123  itgcoscmulx  42611  ibliooicc  42613  stoweidlem11  42653  stoweidlem34  42676  fourierdlem48  42796  fourierdlem49  42797  fourierdlem74  42822  uniimaprimaeqfv  43899  elsetpreimafvssdm  43903  rngcbas  44589  ringcbas  44635  fdivmptf  44955  refdivmptf  44956