MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5ss Structured version   Visualization version   Unicode version

Theorem syl5ss 3455
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
Hypotheses
Ref Expression
syl5ss.1  |-  A  C_  B
syl5ss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5ss
StepHypRef Expression
1 syl5ss.1 . . 3  |-  A  C_  B
21a1i 11 . 2  |-  ( ph  ->  A  C_  B )
3 syl5ss.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3sstrd 3454 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  wereu2  4850  sofld  5303  fvmptss  5981  fimacnv  6035  isofr2  6260  frxp  6933  fnse  6940  smores2  7099  f1imaen2g  7656  domunsncan  7698  fissuni  7905  fipreima  7906  dffi3  7971  marypha1lem  7973  ordtypelem7  8065  ordtypelem8  8066  oismo  8081  unxpwdom2  8129  cantnfres  8208  oemapvali  8215  tskwe  8410  acndom2  8511  dfac2a  8586  dfac12lem2  8600  cfle  8710  cofsmo  8725  coftr  8729  isf34lem5  8834  isf34lem7  8835  isf34lem6  8836  enfin1ai  8840  fin1a2lem12  8867  ttukeylem7  8971  alephexp1  9030  fpwwe2lem13  9093  fpwwe2  9094  canth4  9098  canthwelem  9101  pwfseqlem1  9109  pwfseqlem4  9113  fzossnn0  11980  fsuppmapnn0fiublem  12234  fsuppmapnn0fiub  12235  xptrrel  13093  limsupgle  13584  limsupgre  13591  limsupgreOLD  13592  rlimres  13671  lo1res  13672  lo1resb  13677  rlimresb  13678  o1resb  13679  o1of2  13725  o1rlimmul  13731  isercolllem2  13778  isercoll  13780  climsup  13782  fprodntriv  14045  bitsinvp1  14472  sadcaddlem  14480  sadadd2lem  14482  sadadd3  14484  sadasslem  14493  sadeq  14495  bitsres  14496  smuval2  14505  smupval  14511  smueqlem  14513  smumul  14516  1arith  14920  isstruct2  15179  setscom  15202  ressress  15236  imasvscafn  15492  imasless  15495  mrcssv  15569  isacs1i  15612  mreacs  15613  acsfn  15614  isacs4lem  16463  isacs5lem  16464  mhmima  16659  cntzmhm  17041  f1omvdconj  17136  f1omvdco2  17138  symgsssg  17157  symggen  17160  psgnunilem1  17183  efgval  17416  gsumzaddlem  17603  gsumconst  17616  dmdprdd  17680  dprdfeq0  17704  dprdres  17710  dprdss  17711  dprdz  17712  subgdmdprd  17716  dprddisj2  17721  dprd2dlem1  17723  dprd2da  17724  dprd2d2  17726  dmdprdsplit2lem  17727  lmhmlsp  18321  lsppratlem4  18422  islbs3  18427  lbsextlem3  18432  mplcoe5  18741  mplind  18774  znleval  19174  evpmss  19203  frlmsslsp  19403  lindff1  19427  lindfrn  19428  f1lindf  19429  lindfmm  19434  lsslindf  19437  basdif0  20017  tgcl  20034  ppttop  20071  epttop  20073  ntrin  20125  mretopd  20157  neiptoptop  20196  cnclsi  20337  cnconst2  20348  cnrest2  20351  cnpresti  20353  cnprest2  20355  fiuncmp  20468  connsub  20485  conima  20489  iunconlem  20491  1stcfb  20509  2ndc1stc  20515  2ndcdisj  20520  kgentopon  20602  llycmpkgen2  20614  1stckgenlem  20617  kgencn3  20622  ptclsg  20679  ptcnplem  20685  txtube  20704  hausdiag  20709  txkgen  20716  xkoco1cn  20721  xkoco2cn  20722  xkococnlem  20723  qtoptop2  20763  basqtop  20775  imastopn  20784  hmeores  20835  hmphdis  20860  ptcmpfi  20877  fbssfi  20901  filin  20918  infil  20927  fbasrn  20948  fgtr  20954  elfm  21011  imaelfm  21015  hausflim  21045  flimclslem  21048  fclscmp  21094  cnextcn  21131  tmdgsum2  21160  tgpconcomp  21176  ustexsym  21279  ustund  21285  ustimasn  21292  utoptop  21298  utopbas  21299  restutopopn  21302  blin2  21493  metustexhalf  21620  icccmplem2  21890  icccmplem3  21891  reconnlem2  21894  tchcph  22260  fmcfil  22291  resscdrg  22374  ivthlem2  22452  ivthlem3  22453  ivth2  22455  ovolfiniun  22503  ovoliunlem1  22504  ismbl2  22530  nulmbl2  22539  unmbl  22540  shftmbl  22541  voliunlem1  22552  voliunlem2  22553  ioombl1lem4  22563  uniioombllem4  22593  dyadmbllem  22606  dyadmbl  22607  mbflimsup  22672  mbflimsupOLD  22673  i1fima  22685  i1fima2  22686  i1fadd  22702  itg1addlem4  22706  itg2splitlem  22755  itg2split  22756  ellimc3  22883  limcflflem  22884  limcflf  22885  limcresi  22889  limciun  22898  dvreslem  22913  dvres2lem  22914  dvres  22915  dvaddbr  22941  dvmulbr  22942  dvlip  22994  dvlip2  22996  c1liplem1  22997  dvivthlem1  23009  dvne0  23012  lhop1lem  23014  lhop  23017  dvcnvrelem1  23018  dvcnvrelem2  23019  dvfsumle  23022  dvfsumabs  23024  dvfsumlem2  23028  itgsubstlem  23049  mdegleb  23062  mdeglt  23063  mdegldg  23064  mdegxrcl  23065  mdegcl  23067  ig1peu  23171  ig1peuOLD  23172  reeff1olem  23450  logccv  23657  rlimcnp2  23941  lgamgulmlem2  24004  ppisval  24079  prmdvdsfi  24083  mumul  24157  sqff1o  24158  chtlepsi  24183  chpub  24197  dchrisum0lem2a  24404  pntlem3  24496  ex-res  25940  ghsubgolemOLD  26147  htthlem  26619  chlejb1i  27178  ssmd2  28014  fimarab  28293  gsumle  28591  locfinreflem  28716  sibfof  29222  sitgclbn  29225  sitgaddlemb  29230  eulerpartlemgu  29259  ballotlemsima  29397  ballotlemsimaOLD  29435  bnj1311  29882  erdsze2lem2  29976  iccllyscon  30022  cvmopnlem  30050  msrf  30229  nodenselem6  30624  nofulllem5  30644  neiin  31037  neibastop1  31064  neibastop2lem  31065  topmeet  31069  poimirlem1  31986  poimirlem2  31987  poimirlem3  31988  poimirlem11  31996  poimirlem12  31997  poimirlem16  32001  poimirlem19  32004  poimirlem30  32015  cnambfre  32034  itg2gt0cn  32042  sstotbnd2  32151  sstotbnd3  32153  ssbnd  32165  ismtyima  32180  heibor1lem  32186  pmodlem2  33457  pmodN  33460  diaintclN  34671  djaclN  34749  dibintclN  34780  dicval  34789  dihoml4c  34989  djhcl  35013  isnacs2  35593  isnacs3  35597  diophrw  35646  pellfundre  35774  pellfundge  35775  pellfundlb  35777  pellfundglb  35778  fnwe2lem2  35954  lmhmfgima  35987  hbt  36034  cnvtrcl0  36278  trclrelexplem  36348  relexp0a  36353  rp-imass  36411  climinf  37722  climinfOLD  37723  islptre  37737  limccog  37738  limcleqr  37763  itgcoscmulx  37884  stoweidlem27  37925  dirkercncflem2  38004  fourierdlem38  38046  fourierdlem49  38057  fourierdlem51  38059  fourierdlem54  38062  fourierdlem63  38071  fourierdlem68  38076  fourierdlem69  38077  fourierdlem70  38078  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem80  38088  fourierdlem84  38092  fourierdlem85  38093  fourierdlem88  38096  fourierdlem100  38108  fourierdlem101  38109  fourierdlem104  38112  fourierdlem107  38115  fourierdlem111  38119  fourierdlem112  38120  caragenel2d  38391  hoidmv1lelem3  38453  hspmbllem3  38488  mgmhmima  40075
  Copyright terms: Public domain W3C validator