Theorem sseqtrid 4019

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  iunxdif3  5017  fssdm  6530  fndmdif  6812  fneqeql2  6817  fconst4  6977  isofrlem  7093  f1opw2  7400  fparlem3  7809  fparlem4  7810  fnwelem  7825  frnsuppeq  7842  ecss  8335  pw2f1olem  8621  fopwdom  8625  ssenen  8691  phplem2  8697  ssfi  8738  fiint  8795  f1opwfi  8828  kmlem5  9580  enfin2i  9743  fpwwe2lem6  10057  fpwwe2lem9  10060  tskuni  10205  monoord2  13402  seqz  13419  cshimadifsn0  14192  binom1dif  15188  bpolycl  15406  bpolysum  15407  bpolydiflem  15408  bitsres  15822  prdshom  16740  imasless  16813  cntzval  18451  f1omvdmvd  18571  f1omvdconj  18574  pmtrfb  18593  symggen  18598  symggen2  18599  psgnunilem1  18621  gsumzaddlem  19041  isdrngd  19527  lspextmo  19828  znleval  20701  ordtcld1  21805  ordtcld2  21806  cnpnei  21872  cnntri  21879  cncls2  21881  cncls  21882  cnntr  21883  cncnp  21888  cndis  21899  paste  21902  cmpfi  22016  conncompcld  22042  1stcfb  22053  1stccnp  22070  cldllycmp  22103  llycmpkgen2  22158  kgencn  22164  kgencn3  22166  dfac14lem  22225  txdis1cn  22243  hausdiag  22253  txkgen  22260  qtopval2  22304  basqtop  22319  qtopcld  22321  qtopeu  22324  qtoprest  22325  imastopn  22328  hmeontr  22377  hmeoimaf1o  22378  cmphaushmeo  22408  ordthmeolem  22409  elfm3  22558  rnelfmlem  22560  rnelfm  22561  alexsubALTlem4  22658  cldsubg  22719  tgpconncompeqg  22720  tgpconncomp  22721  qustgpopn  22728  qustgplem  22729  tsmsf1o  22753  ucncn  22894  imasf1oxms  23099  blcld  23115  metustfbas  23167  cfilucfil  23169  metuel2  23175  icchmeo  23545  relcmpcmet  23921  minveclem4a  24033  nulmbl2  24137  icombl  24165  ioombl  24166  uniiccdif  24179  volivth  24208  mbfres2  24246  itg1addlem5  24301  itgsplitioo  24438  dvcobr  24543  dvcnvlem  24573  lhop1lem  24610  lhop  24613  dvcnvrelem2  24615  uc1pval  24733  mon1pval  24735  vieta1lem2  24900  basellem5  25662  f1otrg  26657  axlowdimlem13  26740  axcontlem10  26759  uhgrspansubgr  27073  vtxdun  27263  pthdlem1  27547  eucrct2eupth  28024  ssmd1  30088  mdslj2i  30097  atcvat4i  30174  imadifxp  30351  nfpconfp  30377  ofpreima  30410  ofpreima2  30411  fsuppcurry1  30461  fsuppcurry2  30462  symgcom  30727  symgcom2  30728  pmtrcnel  30733  cycpmfvlem  30754  cycpmfv3  30757  freshmansdream  30859  qtophaus  31100  reff  31103  locfinreflem  31104  hauseqcn  31138  indpreima  31284  indf1ofs  31285  oms0  31555  eulerpartlemv  31622  eulerpartlemb  31626  eulerpartlemr  31632  eulerpartlemgs2  31638  eulerpartlemn  31639  ballotlemro  31780  bnj1253  32289  bnj1280  32292  pthhashvtx  32374  acycgr0v  32395  prclisacycgr  32398  subfacp1lem3  32429  cvmscld  32520  cvmsss2  32521  cvmliftmolem1  32528  cvmliftlem7  32538  cvmlift2lem9  32558  cvmlift3lem7  32572  fnessref  33705  tailf  33723  poimirlem3  34910  mbfresfi  34953  cnambfre  34955  itg2addnclem2  34959  mettrifi  35047  ismtyres  35101  isdrngo2  35251  diaintclN  38209  dibintclN  38318  dihintcl  38495  dochocss  38517  mapdunirnN  38801  pw2f1ocnv  39683  wessf1ornlem  41494  monoord2xrv  41809  itgcoscmulx  42303  ibliooicc  42305  stoweidlem11  42345  stoweidlem34  42368  fourierdlem48  42488  fourierdlem49  42489  fourierdlem74  42514  uniimaprimaeqfv  43591  elsetpreimafvssdm  43595  rngcbas  44285  ringcbas  44331  fdivmptf  44650  refdivmptf  44651