Theorem syl5eqssr 3650

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 2631	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqssr.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	syl5eqss 3649	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  relcnvtr  5655  fimacnvdisj  6083  dffv2  6271  fimacnv  6347  f1ompt  6382  abnexg  6964  fnwelem  7292  tfrlem15  7488  omxpenlem  8061  hartogslem1  8447  infxpidm2  8840  alephgeom  8905  infenaleph  8914  cfflb  9081  pwfseqlem5  9485  imasvscafn  16197  mrieqvlemd  16289  cnvps  17212  dirdm  17234  tsrdir  17238  frmdss2  17400  iinopn  20707  neitr  20984  xkococnlem  21462  tgpconncomp  21916  trcfilu  22098  mbfconstlem  23396  itg2seq  23509  limcdif  23640  dvres2lem  23674  c1lip3  23762  lhop  23779  plyeq0  23967  dchrghm  24981  uspgrupgrushgr  26072  upgrreslem  26196  umgrreslem  26197  umgrres1  26206  umgr2v2e  26421  chssoc  28355  hauseqcn  29941  carsgclctunlem3  30382  cvmliftmolem1  31263  cvmlift2lem9a  31285  cvmlift2lem9  31293  cnres2  33562  rngunsnply  37743  proot1hash  37778  clcnvlem  37930  cnvtrcl0  37933  trrelsuperrel2dg  37963  brtrclfv2  38019  fourierdlem92  40415  vsetrec  42446