Theorem syl5ss 2105

Description: A chained subclass and equality deduction.

Hypotheses

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

Assertion

Ref	Expression
syl5ss	|- (ph -> C (_ B)

Proof of Theorem syl5ss

Step	Hyp	Ref	Expression
1		syl5ss.1	. 2 |- (ph -> A (_ B)
2		syl5ss.2	. . 3 |- C = A
3	2	sseq1i 2085	. 2 |- (C (_ B <-> A (_ B)
4	1, 3	sylibr 200	1 |- (ph -> C (_ B)

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

This theorem is referenced by:  syl5ssr 2106  suceloni 3062  xpsspw 3257  cotr 3436  cnvsym 3437  fun 3641  fopab2 3823  1stcof 4101  rankr1 4674  rankr1id 4697  oncard 4829  cflecard 4912  peano5nn 5926  peano5uz 6203  uzwo3lem1 6216  uzwo3lem2 6217  sh0let 9364  mdslmd3 10259  ghomfo 10391  homcard 10539

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