Theorem syl5eqssr 3613

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 2619	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqssr.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	syl5eqss 3612	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:  relcnvtr  5572  fimacnvdisj  5996  dffv2  6181  fimacnv  6255  f1ompt  6290  fnwelem  7179  tfrlem15  7375  omxpenlem  7946  hartogslem1  8330  infxpidm2  8723  alephgeom  8788  infenaleph  8797  cfflb  8964  pwfseqlem5  9364  imasvscafn  16020  mrieqvlemd  16112  cnvps  17035  dirdm  17057  tsrdir  17061  frmdss2  17223  iinopn  20532  neitr  20794  xkococnlem  21272  tgpconcomp  21726  trcfilu  21908  mbfconstlem  23202  itg2seq  23315  limcdif  23446  dvres2lem  23480  c1lip3  23566  lhop  23583  plyeq0  23771  dchrghm  24781  chssoc  27739  hauseqcn  29269  carsgclctunlem3  29709  cvmliftmolem1  30517  cvmlift2lem9a  30539  cvmlift2lem9  30547  cnres2  32732  rngunsnply  36762  proot1hash  36797  clcnvlem  36949  cnvtrcl0  36952  trrelsuperrel2dg  36982  brtrclfv2  37038  fourierdlem92  39091  umgrres1  40533  umgr2v2e  40741  vsetrec  42245