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

Theorem syl5ss 3351
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 3350 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3312
This theorem is referenced by:  wereu2  4571  sofld  5310  fvmptss  5805  fimacnv  5854  isofr2  6056  frxp  6448  fnse  6455  smores2  6608  f1imaen2g  7160  domunsncan  7200  fissuni  7403  fipreima  7404  dffi3  7428  marypha1lem  7430  ordtypelem7  7485  ordtypelem8  7486  oismo  7501  unxpwdom2  7548  oemapvali  7632  mapfien  7645  tskwe  7829  acndom2  7927  dfac2a  8002  dfac12lem2  8016  cfle  8126  cofsmo  8141  coftr  8145  isf34lem5  8250  isf34lem7  8251  isf34lem6  8252  enfin1ai  8256  fin1a2lem12  8283  ttukeylem7  8387  alephexp1  8446  fpwwe2lem13  8509  fpwwe2  8510  canth4  8514  canthwelem  8517  pwfseqlem1  8525  pwfseqlem4  8529  limsupgle  12263  limsupgre  12267  rlimres  12344  lo1res  12345  lo1resb  12350  rlimresb  12351  o1resb  12352  o1of2  12398  o1rlimmul  12404  isercolllem2  12451  isercoll  12453  climsup  12455  bitsinvp1  12953  sadcaddlem  12961  sadadd2lem  12963  sadadd3  12965  sadasslem  12974  sadeq  12976  bitsres  12977  smuval2  12986  smupval  12992  smueqlem  12994  smumul  12997  1arith  13287  isstruct2  13470  setscom  13489  ressress  13518  imasvscafn  13754  imasless  13757  mrcssv  13831  isacs1i  13874  mreacs  13875  acsfn  13876  isacs4lem  14586  isacs5lem  14587  mhmima  14755  cntzmhm  15129  efgval  15341  gsumzaddlem  15518  dmdprdd  15552  dprdfeq0  15572  dprdres  15578  dprdss  15579  dprdz  15580  subgdmdprd  15584  dprddisj2  15589  dprd2dlem1  15591  dprd2da  15592  dprd2d2  15594  dmdprdsplit2lem  15595  lmhmlsp  16117  lsppratlem4  16214  islbs3  16219  lbsextlem3  16224  mplcoe2  16522  mplind  16554  znleval  16827  basdif0  17010  tgcl  17026  ppttop  17063  epttop  17065  ntrin  17117  mretopd  17148  neiptoptop  17187  islp3  17202  cnclsi  17328  cnconst2  17339  cnrest  17341  cnrest2  17342  cnpresti  17344  cnprest2  17346  fiuncmp  17459  connsub  17476  conima  17480  iunconlem  17482  1stcfb  17500  2ndc1stc  17506  2ndcdisj  17511  kgentopon  17562  llycmpkgen2  17574  1stckgenlem  17577  kgencn3  17582  ptclsg  17639  ptcnplem  17645  txtube  17664  hausdiag  17669  txkgen  17676  xkoco1cn  17681  xkoco2cn  17682  xkococnlem  17683  qtoptop2  17723  basqtop  17735  imastopn  17744  hmeores  17795  hmphdis  17820  ptcmpfi  17837  fbssfi  17861  filin  17878  infil  17887  fbasrn  17908  fgtr  17914  elfm  17971  imaelfm  17975  hausflim  18005  flimclslem  18008  fclscmp  18054  cnextcn  18090  tmdgsum2  18118  tgpconcomp  18134  tsmsres  18165  ustexsym  18237  ustund  18243  ustimasn  18250  utoptop  18256  utopbas  18257  restutopopn  18260  blin2  18451  metustexhalfOLD  18585  metustexhalf  18586  icccmplem2  18846  icccmplem3  18847  reconnlem2  18850  tchcph  19186  fmcfil  19217  resscdrg  19304  ivthlem2  19341  ivthlem3  19342  ivth2  19344  ovolfiniun  19389  ovoliunlem1  19390  ismbl2  19415  nulmbl2  19423  unmbl  19424  shftmbl  19425  voliunlem1  19436  voliunlem2  19437  ioombl1lem4  19447  uniioombllem4  19470  dyadmbllem  19483  dyadmbl  19484  mbflimsup  19550  i1fima  19562  i1fima2  19563  i1fadd  19579  itg1addlem4  19583  itg2splitlem  19632  itg2split  19633  ellimc3  19758  limcflflem  19759  limcflf  19760  limcresi  19764  limciun  19773  dvreslem  19788  dvres2lem  19789  dvres  19790  dvaddbr  19816  dvmulbr  19817  dvlip  19869  dvlip2  19871  c1liplem1  19872  dvivthlem1  19884  dvne0  19887  lhop1lem  19889  lhop  19892  dvcnvrelem1  19893  dvcnvrelem2  19894  dvfsumle  19897  dvfsumabs  19899  dvfsumlem2  19903  itgsubstlem  19924  mdegleb  19979  mdeglt  19980  mdegldg  19981  mdegxrcl  19982  mdegcl  19984  ig1peu  20086  reeff1olem  20354  logccv  20546  rlimcnp2  20797  ppisval  20878  prmdvdsfi  20882  mumul  20956  sqff1o  20957  chtlepsi  20982  chpub  20996  dchrisum0lem2a  21203  pntlem3  21295  ex-res  21741  ghsubgolem  21950  htthlem  22412  chlejb1i  22970  ssmd2  23807  sibfof  24646  sitgclbn  24649  ballotlemsima  24765  lgamgulmlem2  24806  erdsze2lem2  24882  iccllyscon  24929  cvmopnlem  24957  relexpdm  25127  relexprn  25128  fprodntriv  25260  nodenselem6  25633  nofulllem5  25653  cnambfre  26245  itg2gt0cn  26250  neiin  26316  neibastop1  26369  neibastop2lem  26370  topmeet  26374  sstotbnd2  26464  sstotbnd3  26466  ssbnd  26478  ismtyima  26493  heibor1lem  26499  isnacs2  26741  isnacs3  26745  diophrw  26798  pellfundre  26925  pellfundge  26926  pellfundlb  26928  pellfundglb  26929  fnwe2lem2  27107  lmhmfgima  27140  frlmsslsp  27206  lindff1  27248  lindfrn  27249  f1lindf  27250  lindfmm  27255  lsslindf  27258  hbt  27292  f1omvdconj  27347  f1omvdco2  27349  symgsssg  27366  symggen  27369  psgnunilem1  27374  climinf  27689  stoweidlem27  27733  fzossnn0  28097  bnj1311  29320  pmodlem2  30571  pmodN  30574  diaintclN  31783  djaclN  31861  dibintclN  31892  dicval  31901  dihoml4c  32101  djhcl  32125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator