Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5eqss GIF version

Theorem syl5eqss 3073
 Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqss.1 𝐴 = 𝐵
syl5eqss.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
syl5eqss (𝜑𝐴𝐶)

Proof of Theorem syl5eqss
StepHypRef Expression
1 syl5eqss.2 . 2 (𝜑𝐵𝐶)
2 syl5eqss.1 . . 3 𝐴 = 𝐵
32sseq1i 3053 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 133 1 (𝜑𝐴𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1290   ⊆ wss 3002 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071 This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3008  df-ss 3015 This theorem is referenced by:  syl5eqssr  3074  inss  3232  difsnss  3591  tpssi  3611  peano5  4428  xpsspw  4565  iotanul  5010  iotass  5012  fun  5198  fun11iun  5289  fvss  5334  fmpt  5465  fliftrel  5587  opabbrex  5709  1stcof  5950  2ndcof  5951  tfrlemibacc  6107  tfrlemibfn  6109  tfr1onlemssrecs  6120  tfr1onlembacc  6123  tfr1onlembfn  6125  tfrcllemssrecs  6133  tfrcllembacc  6136  tfrcllembfn  6138  caucvgprlemladdrl  7300  peano5nnnn  7490  peano5nni  8488  un0addcl  8769  un0mulcl  8770  strleund  11645  bj-omtrans  12155
 Copyright terms: Public domain W3C validator