Theorem eqsstrrid 4029

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

Hypotheses

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

Assertion

Ref	Expression
eqsstrrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrid

Step	Hyp	Ref	Expression
1		eqsstrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2742	. 2 ⊢ 𝐴 = 𝐵
3		eqsstrrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrid 4028	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3953  df-ss 3963

This theorem is referenced by:  relcnvtrg  6257  fimacnvdisj  6759  dffv2  6975  fimacnvOLD  7060  f1ompt  7098  abnexg  7730  fnwelem  8104  tfrlem15  8379  omxpenlem  9061  hartogslem1  9524  ttrcltr  9698  dfttrcl2  9706  infxpidm2  9999  alephgeom  10064  infenaleph  10073  cfflb  10241  pwfseqlem5  10645  imasvscafn  17470  mrieqvlemd  17560  cnvps  18518  dirdm  18540  tsrdir  18544  frmdss2  18731  subdrgint  20396  iinopn  22373  neitr  22653  xkococnlem  23132  tgpconncomp  23586  trcfilu  23768  mbfconstlem  25113  itg2seq  25229  limcdif  25362  dvres2lem  25396  c1lip3  25485  lhop  25502  plyeq0  25694  dchrghm  26726  negsbdaylem  27497  precsexlem10  27629  uspgrupgrushgr  28404  upgrreslem  28528  umgrreslem  28529  umgrres1  28538  umgr2v2e  28749  chssoc  30714  gsumhashmul  32179  pmtrcnelor  32223  tocycfvres1  32240  tocycfvres2  32241  dimkerim  32650  hauseqcn  32809  carsgclctunlem3  33250  cvmliftmolem1  34203  cvmlift2lem9a  34225  cvmlift2lem9  34233  cnres2  36537  rngunsnply  41786  proot1hash  41813  omabs2  41953  clcnvlem  42245  cnvtrcl0  42248  trrelsuperrel2dg  42293  brtrclfv2  42349  imo72b2lem1  42792  fourierdlem92  44787  vsetrec  47588