Theorem eqsstr3d 2096

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 1480	. 2 |- (ph -> A = B)
3		eqsstr3d.2	. 2 |- (ph -> B (_ C)
4	2, 3	eqsstrd 2095	1 |- (ph -> A (_ C)

Syntax hints:   -> wi 3   = wceq 956   (_ wss 2047

This theorem is referenced by:  sspr 2475  ssxpr 3475  oaword1 4186  omword2 4205  r1val1 4658  rankxpl 4710  rankxplim3 4714  basgen2t 7639  caussi 7954  sspg 8387  ssps 8389  sspn 8395  kbass5t 10053  mdslj1 10246  mdslj2 10247  sh1dle 10278  shatomistic 10288  sumdmdi 10342

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

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

Copyright terms: Public domain