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

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

Proof of Theorem sseqtrid
StepHypRef Expression
1 sseqtrid.2 . 2 (𝜑𝐴 = 𝐶)
2 sseqtrid.1 . 2 𝐵𝐴
3 sseq2 3171 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 294 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 411 1 (𝜑𝐵𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  wss 3121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  fssdm  5360  fndmdif  5598  fneqeql2  5602  fconst4m  5713  f1opw2  6052  ecss  6550  fopwdom  6810  ssenen  6825  phplem2  6827  fiintim  6902  casefun  7058  caseinj  7062  djufun  7077  djuinj  7079  nn0supp  9174  monoord2  10420  binom1dif  11437  cnpnei  12934  cnntri  12939  cnntr  12940  cncnp  12945  cndis  12956  txdis1cn  12993  hmeontr  13028  hmeoimaf1o  13029  dvcoapbr  13386
  Copyright terms: Public domain W3C validator