Theorem eqsstrrd 3230

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

Ref	Expression
eqsstrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2211	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3229	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 3166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  ssxpbm  5118  ssxp1  5119  ssxp2  5120  suppssof1  6176  tfrlemiubacc  6416  tfr1onlemubacc  6432  tfrcllemubacc  6445  oaword1  6557  phplem4dom  6959  fisseneq  7031  nnnninfeq2  7231  archnqq  7530  hashdmprop2dom  10989  imasaddfnlemg  13146  resmhm2  13320  ringidss  13791  subrg1  13993  subrgdvds  13997  subrguss  13998  subrginv  13999  islss3  14141  lspsnneg  14182  epttop  14562  metequiv2  14968  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  nnsf  15942