Theorem syl5sseq 3616

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
syl5sseq.1	⊢ 𝐵 ⊆ 𝐴
syl5sseq.2	⊢ (𝜑 → 𝐴 = 𝐶)

Assertion

Ref	Expression
syl5sseq	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem syl5sseq

Step	Hyp	Ref	Expression
1		syl5sseq.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		syl5sseq.1	. 2 ⊢ 𝐵 ⊆ 𝐴
3		sseq2 3590	. . 3 ⊢ (𝐴 = 𝐶 → (𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐶))
4	3	biimpa 500	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐶)
5	1, 2, 4	sylancl 693	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  iunxdif3  4542  fndmdif  6229  fneqeql2  6234  fconst4  6383  isofrlem  6490  f1opw2  6786  fparlem3  7166  fparlem4  7167  fnwelem  7179  frnsuppeq  7194  ecss  7675  pw2f1olem  7949  fopwdom  7953  ssenen  8019  phplem2  8025  ssfi  8065  fiint  8122  f1opwfi  8153  fisuppfi  8166  wemapso  8339  wemapso2lem  8340  cantnfcl  8447  cantnfle  8451  cantnflt  8452  cantnff  8454  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cantnflem3  8471  cnfcomlem  8479  cnfcom  8480  cnfcom2lem  8481  cnfcom3lem  8483  cnfcom3  8484  kmlem5  8859  enfin2i  9026  fin1a2lem7  9111  fpwwe2lem6  9336  fpwwe2lem9  9339  tskuni  9484  monoord2  12694  seqz  12711  cshimadifsn0  13427  isercolllem2  14244  isercolllem3  14245  fsumss  14303  binom1dif  14404  fprodss  14517  bpolycl  14622  bpolysum  14623  bpolydiflem  14624  bitsres  15033  vdwlem1  15523  vdwlem5  15527  vdwlem6  15528  prdshom  15950  imasless  16023  ghmpreima  17505  cntzval  17577  f1omvdmvd  17686  f1omvdconj  17689  pmtrfb  17708  pmtrfconj  17709  symggen  17713  symggen2  17714  psgnunilem1  17736  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumzmhm  18160  gsumzoppg  18167  gsum2d  18194  dpjidcl  18280  isdrngd  18595  lmhmpreima  18869  lspextmo  18877  mplcoe1  19286  mplcoe5  19289  psr1baslem  19376  gsumfsum  19632  znleval  19722  regsumsupp  19787  frlmlbs  19955  mdetdiaglem  20223  ordtcld1  20811  ordtcld2  20812  cnpnei  20878  cnclima  20882  iscncl  20883  cnntri  20885  cnclsi  20886  cncls2  20887  cncls  20888  cnntr  20889  cncnp  20894  cndis  20905  paste  20908  cmpfi  21021  concompcld  21047  1stcfb  21058  1stccnp  21075  cldllycmp  21108  llycmpkgen2  21163  kgencn  21169  kgencn3  21171  dfac14lem  21230  txcnmpt  21237  txdis1cn  21248  hausdiag  21258  txkgen  21265  qtopval2  21309  basqtop  21324  qtopcld  21326  qtopcn  21327  qtopeu  21329  qtoprest  21330  imastopn  21333  hmeontr  21382  hmeoimaf1o  21383  cmphaushmeo  21413  ordthmeolem  21414  elfm3  21564  rnelfmlem  21566  rnelfm  21567  fmfnfmlem4  21571  alexsubALTlem4  21664  clssubg  21722  cldsubg  21724  tgpconcompeqg  21725  tgpconcomp  21726  tgphaus  21730  qustgpopn  21733  qustgplem  21734  tsmsgsum  21752  tsmsf1o  21758  ucncn  21899  xmeter  22048  imasf1oxms  22104  blcld  22120  metustss  22166  metustexhalf  22171  metustfbas  22172  cfilucfil  22174  metuel2  22180  restmetu  22185  icchmeo  22548  relcmpcmet  22923  rrxcph  22988  rrxsuppss  22994  minveclem4a  23009  nulmbl2  23111  icombl  23139  ioombl  23140  uniiccdif  23152  volivth  23181  mbfres2  23218  itg1addlem5  23273  itgsplitioo  23410  dvcobr  23515  dvcnvlem  23543  lhop1lem  23580  lhop  23583  dvcnvrelem2  23585  mdegfval  23626  mdegleb  23628  mdegldg  23630  deg1mul3le  23680  uc1pval  23703  mon1pval  23705  plyeq0lem  23770  dgrcl  23793  dgrub  23794  dgrlb  23796  vieta1lem1  23869  vieta1lem2  23870  basellem5  24611  f1otrg  25551  axlowdimlem13  25634  axcontlem10  25653  vdgrun  26428  vdgrfiun  26429  eupares  26502  eupath2lem3  26506  ssmd1  28554  mdslj2i  28563  atcvat4i  28640  imadifxp  28796  ofpreima  28848  ofpreima2  28849  qtophaus  29231  reff  29234  locfinreflem  29235  hauseqcn  29269  indpreima  29414  indf1ofs  29415  oms0  29686  sibfof  29729  eulerpartlemsv2  29747  eulerpartlemsf  29748  eulerpartlemv  29753  eulerpartlemb  29757  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemgu  29766  eulerpartlemgs2  29769  eulerpartlemn  29770  ballotlemro  29911  bnj1253  30339  bnj1280  30342  subfacp1lem3  30418  cvmscld  30509  cvmsss2  30510  cvmliftmolem1  30517  cvmliftlem7  30527  cvmlift2lem9  30547  cvmlift3lem6  30560  cvmlift3lem7  30561  fnessref  31522  tailf  31540  poimirlem3  32582  mbfresfi  32626  cnambfre  32628  itg2addnclem  32631  itg2addnclem2  32632  mettrifi  32723  ismtyres  32777  isdrngo2  32927  keridl  33001  diaintclN  35365  dibintclN  35474  dihintcl  35651  dochocss  35673  mapdunirnN  35957  ismrcd1  36279  istopclsd  36281  pw2f1ocnv  36622  pwfi2f1o  36684  wessf1ornlem  38366  itgcoscmulx  38861  ibliooicc  38863  stoweidlem11  38904  stoweidlem34  38927  fourierdlem48  39047  fourierdlem49  39048  fourierdlem74  39073  uhgrspansubgr  40515  vtxdun  40696  pthdlem1  40972  eucrct2eupth  41413  rngcbas  41757  ringcbas  41803  fdivmptf  42133  refdivmptf  42134