Theorem syl5eqssr 3908

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

Ref	Expression
syl5eqssr	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl5eqssr

Step	Hyp	Ref	Expression
1		syl5eqssr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2787	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqssr.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	syl5eqss 3907	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1507   ⊆ wss 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-in 3838  df-ss 3845

This theorem is referenced by:  relcnvtr  5960  fimacnvdisj  6388  dffv2  6586  fimacnv  6666  f1ompt  6700  abnexg  7297  fnwelem  7632  tfrlem15  7834  omxpenlem  8416  hartogslem1  8803  infxpidm2  9239  alephgeom  9304  infenaleph  9313  cfflb  9481  pwfseqlem5  9885  imasvscafn  16669  mrieqvlemd  16761  cnvps  17683  dirdm  17705  tsrdir  17709  frmdss2  17872  subdrgint  19307  iinopn  21217  neitr  21495  xkococnlem  21974  tgpconncomp  22427  trcfilu  22609  mbfconstlem  23934  itg2seq  24049  limcdif  24180  dvres2lem  24214  c1lip3  24302  lhop  24319  plyeq0  24507  dchrghm  25537  uspgrupgrushgr  26668  upgrreslem  26792  umgrreslem  26793  umgrres1  26802  umgr2v2e  27013  chssoc  29057  dimkerim  30652  hauseqcn  30782  carsgclctunlem3  31223  cvmliftmolem1  32113  cvmlift2lem9a  32135  cvmlift2lem9  32143  cnres2  34483  rngunsnply  39169  proot1hash  39196  clcnvlem  39346  cnvtrcl0  39349  trrelsuperrel2dg  39379  brtrclfv2  39435  fourierdlem92  41915  vsetrec  44173