Theorem syl5ss 2108

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 2088	. 2 |- (C (_ B <-> A (_ B)
4	1, 3	sylibr 200	1 |- (ph -> C (_ B)

Syntax hints:   -> wi 3   = wceq 958   (_ wss 2050

This theorem is referenced by:  syl5ssr 2109  suceloni 3068  xpsspw 3263  cotr 3442  cnvsym 3443  fun 3647  fopab2 3829  1stcof 4107  rankr1 4684  rankr1id 4707  oncard 4839  cflecard 4924  peano5nn 5928  peano5uz 6205  uzwo3lem1 6218  uzwo3lem2 6219  sh0let 9359  mdslmd3 10254  ghomfo 10386  homcard 10525

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain