Theorem eqsstr3d 2094

Description: Substitution of equality into a subclass relationship.

Hypotheses

Ref	Expression
eqsstr3d.1	|- (ph -> B = A)
eqsstr3d.2	|- (ph -> B (_ C)

Assertion

Ref	Expression
eqsstr3d	|- (ph -> A (_ C)

Proof of Theorem eqsstr3d

Step	Hyp	Ref	Expression
1		eqsstr3d.1	. . 3 |- (ph -> B = A)
2	1	eqcomd 1479	. 2 |- (ph -> A = B)
3		eqsstr3d.2	. 2 |- (ph -> B (_ C)
4	2, 3	eqsstrd 2093	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 955   (_ wss 2045

This theorem is referenced by:  sspr 2473  ssxpr 3472  oaword1 4183  omword2 4202  r1val1 4645  rankxpl 4697  rankxplim3 4701  basgen2t 7618  caussi 7937  sspg 8373  ssps 8375  sspn 8381  kbass5t 10044  mdslj1 10237  mdslj2 10238  sh1dle 10269  shatomistic 10279  sumdmdi 10333

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2049  df-ss 2051

Copyright terms: Public domain