Theorem syl5sseq 3872

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

Syntax hints:   → wi 4   = wceq 1601   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  iunxdif3  4840  fssdm  6307  fndmdif  6584  fneqeql2  6589  fconst4  6750  isofrlem  6862  f1opw2  7165  fparlem3  7560  fparlem4  7561  fnwelem  7573  frnsuppeq  7588  ecss  8070  pw2f1olem  8352  fopwdom  8356  ssenen  8422  phplem2  8428  ssfi  8468  fiint  8525  f1opwfi  8558  kmlem5  9311  enfin2i  9478  fpwwe2lem6  9792  fpwwe2lem9  9795  tskuni  9940  monoord2  13150  seqz  13167  cshimadifsn0  13981  binom1dif  14969  bpolycl  15185  bpolysum  15186  bpolydiflem  15187  bitsres  15601  prdshom  16513  imasless  16586  cntzval  18137  f1omvdmvd  18246  f1omvdconj  18249  pmtrfb  18268  symggen  18273  symggen2  18274  psgnunilem1  18296  gsumzaddlem  18707  isdrngd  19164  lspextmo  19451  znleval  20298  ordtcld1  21409  ordtcld2  21410  cnpnei  21476  cnntri  21483  cncls2  21485  cncls  21486  cnntr  21487  cncnp  21492  cndis  21503  paste  21506  cmpfi  21620  conncompcld  21646  1stcfb  21657  1stccnp  21674  cldllycmp  21707  llycmpkgen2  21762  kgencn  21768  kgencn3  21770  dfac14lem  21829  txdis1cn  21847  hausdiag  21857  txkgen  21864  qtopval2  21908  basqtop  21923  qtopcld  21925  qtopeu  21928  qtoprest  21929  imastopn  21932  hmeontr  21981  hmeoimaf1o  21982  cmphaushmeo  22012  ordthmeolem  22013  elfm3  22162  rnelfmlem  22164  rnelfm  22165  alexsubALTlem4  22262  cldsubg  22322  tgpconncompeqg  22323  tgpconncomp  22324  qustgpopn  22331  qustgplem  22332  tsmsf1o  22356  ucncn  22497  imasf1oxms  22702  blcld  22718  metustfbas  22770  cfilucfil  22772  metuel2  22778  icchmeo  23148  relcmpcmet  23524  minveclem4a  23636  nulmbl2  23740  icombl  23768  ioombl  23769  uniiccdif  23782  volivth  23811  mbfres2  23849  itg1addlem5  23904  itgsplitioo  24041  dvcobr  24146  dvcnvlem  24176  lhop1lem  24213  lhop  24216  dvcnvrelem2  24218  uc1pval  24336  mon1pval  24338  vieta1lem2  24503  basellem5  25263  f1otrg  26220  axlowdimlem13  26303  axcontlem10  26322  uhgrspansubgr  26638  vtxdun  26829  pthdlem1  27118  eucrct2eupthOLD  27650  eucrct2eupth  27651  ssmd1  29742  mdslj2i  29751  atcvat4i  29828  imadifxp  29977  ofpreima  30030  ofpreima2  30031  qtophaus  30501  reff  30504  locfinreflem  30505  hauseqcn  30539  indpreima  30685  indf1ofs  30686  oms0  30957  eulerpartlemv  31024  eulerpartlemb  31028  eulerpartlemr  31034  eulerpartlemgs2  31040  eulerpartlemn  31041  ballotlemro  31183  bnj1253  31684  bnj1280  31687  subfacp1lem3  31763  cvmscld  31854  cvmsss2  31855  cvmliftmolem1  31862  cvmliftlem7  31872  cvmlift2lem9  31892  cvmlift3lem7  31906  fnessref  32940  tailf  32958  poimirlem3  34040  mbfresfi  34083  cnambfre  34085  itg2addnclem2  34089  mettrifi  34179  ismtyres  34233  isdrngo2  34383  diaintclN  37214  dibintclN  37323  dihintcl  37500  dochocss  37522  mapdunirnN  37806  pw2f1ocnv  38567  wessf1ornlem  40298  monoord2xrv  40623  itgcoscmulx  41116  ibliooicc  41118  stoweidlem11  41159  stoweidlem34  41182  fourierdlem48  41302  fourierdlem49  41303  fourierdlem74  41328  rngcbas  42984  ringcbas  43030  fdivmptf  43354  refdivmptf  43355