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

Theorem syl5sseq 3077
 Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseq.1 𝐵𝐴
syl5sseq.2 (𝜑𝐴 = 𝐶)
Assertion
Ref Expression
syl5sseq (𝜑𝐵𝐶)

Proof of Theorem syl5sseq
StepHypRef Expression
1 syl5sseq.2 . 2 (𝜑𝐴 = 𝐶)
2 syl5sseq.1 . 2 𝐵𝐴
3 sseq2 3051 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 291 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 405 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:  fssdm  5190  fndmdif  5420  fneqeql2  5424  fconst4m  5533  f1opw2  5866  ecss  6349  fopwdom  6608  ssenen  6623  phplem2  6625  fiintim  6695  casefun  6832  caseinj  6836  djufun  6842  djuinj  6844  nn0supp  8788  monoord2  9968  binom1dif  10944
 Copyright terms: Public domain W3C validator