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

Theorem sseqtrid 3178
 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 3152 . . 3
43biimpa 294 . 2
51, 2, 4sylancl 410 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1335   wss 3102 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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115 This theorem is referenced by:  fssdm  5331  fndmdif  5569  fneqeql2  5573  fconst4m  5684  f1opw2  6020  ecss  6514  fopwdom  6774  ssenen  6789  phplem2  6791  fiintim  6866  casefun  7019  caseinj  7023  djufun  7038  djuinj  7040  nn0supp  9125  monoord2  10358  binom1dif  11366  cnpnei  12579  cnntri  12584  cnntr  12585  cncnp  12590  cndis  12601  txdis1cn  12638  hmeontr  12673  hmeoimaf1o  12674  dvcoapbr  13031
 Copyright terms: Public domain W3C validator