Theorem sseqtrid 3939

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-in 3860  df-ss 3870

This theorem is referenced by:  iunxdif3  4990  fssdm  6535  fndmdif  6832  fneqeql2  6837  fconst4  7000  isofrlem  7119  f1opw2  7429  fparlem3  7848  fparlem4  7849  fnwelem  7864  frnsuppeq  7883  frnsuppeqg  7884  ecss  8379  pw2f1olem  8683  fopwdom  8687  ssenen  8754  phplem2  8760  ssfiOLD  8829  fiint  8882  f1opwfi  8914  kmlem5  9667  enfin2i  9834  fpwwe2lem5  10148  fpwwe2lem8  10151  tskuni  10296  monoord2  13506  seqz  13523  cshimadifsn0  14294  binom1dif  15294  bpolycl  15511  bpolysum  15512  bpolydiflem  15513  bitsres  15929  prdshom  16856  imasless  16929  cntzval  18582  f1omvdmvd  18702  f1omvdconj  18705  pmtrfb  18724  symggen  18729  symggen2  18730  psgnunilem1  18752  gsumzaddlem  19173  isdrngd  19659  lspextmo  19960  znleval  20386  ordtcld1  21961  ordtcld2  21962  cnpnei  22028  cnntri  22035  cncls2  22037  cncls  22038  cnntr  22039  cncnp  22044  cndis  22055  paste  22058  cmpfi  22172  conncompcld  22198  1stcfb  22209  1stccnp  22226  cldllycmp  22259  llycmpkgen2  22314  kgencn  22320  kgencn3  22322  dfac14lem  22381  txdis1cn  22399  hausdiag  22409  txkgen  22416  qtopval2  22460  basqtop  22475  qtopcld  22477  qtopeu  22480  qtoprest  22481  imastopn  22484  hmeontr  22533  hmeoimaf1o  22534  cmphaushmeo  22564  ordthmeolem  22565  elfm3  22714  rnelfmlem  22716  rnelfm  22717  alexsubALTlem4  22814  cldsubg  22875  tgpconncompeqg  22876  tgpconncomp  22877  qustgpopn  22884  qustgplem  22885  tsmsf1o  22909  ucncn  23050  imasf1oxms  23255  blcld  23271  metustfbas  23323  cfilucfil  23325  metuel2  23331  icchmeo  23706  relcmpcmet  24083  minveclem4a  24195  nulmbl2  24301  icombl  24329  ioombl  24330  uniiccdif  24343  volivth  24372  mbfres2  24410  itg1addlem5  24466  itgsplitioo  24603  dvcobr  24711  dvcnvlem  24741  lhop1lem  24778  lhop  24781  dvcnvrelem2  24783  uc1pval  24905  mon1pval  24907  vieta1lem2  25072  basellem5  25835  f1otrg  26830  axlowdimlem13  26913  axcontlem10  26932  uhgrspansubgr  27246  vtxdun  27436  pthdlem1  27720  eucrct2eupth  28195  ssmd1  30259  mdslj2i  30268  atcvat4i  30345  imadifxp  30527  nfpconfp  30554  2ndresdju  30573  ofpreima  30590  ofpreima2  30591  fsuppcurry1  30648  fsuppcurry2  30649  gsumpart  30905  symgcom  30942  symgcom2  30943  pmtrcnel  30948  cycpmfvlem  30969  cycpmfv3  30972  freshmansdream  31074  elrspunidl  31191  idlinsubrg  31193  qtophaus  31371  reff  31374  locfinreflem  31375  zarcmplem  31416  hauseqcn  31433  indpreima  31576  indf1ofs  31577  oms0  31847  eulerpartlemv  31914  eulerpartlemb  31918  eulerpartlemr  31924  eulerpartlemgs2  31930  eulerpartlemn  31931  ballotlemro  32072  bnj1253  32581  bnj1280  32584  pthhashvtx  32673  acycgr0v  32694  prclisacycgr  32697  subfacp1lem3  32728  cvmscld  32819  cvmsss2  32820  cvmliftmolem1  32827  cvmliftlem7  32837  cvmlift2lem9  32857  cvmlift3lem7  32871  fnessref  34202  tailf  34220  poimirlem3  35436  mbfresfi  35479  cnambfre  35481  itg2addnclem2  35485  mettrifi  35571  ismtyres  35622  isdrngo2  35772  diaintclN  38728  dibintclN  38837  dihintcl  39014  dochocss  39036  mapdunirnN  39320  pw2f1ocnv  40472  wessf1ornlem  42301  monoord2xrv  42605  itgcoscmulx  43093  ibliooicc  43095  stoweidlem11  43135  stoweidlem34  43158  fourierdlem48  43278  fourierdlem49  43279  fourierdlem74  43304  uniimaprimaeqfv  44416  elsetpreimafvssdm  44420  rngcbas  45105  ringcbas  45151  fdivmptf  45469  refdivmptf  45470  iscnrm3llem2  45814