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

Theorem syl5ss 3355
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 3354 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  wereu2  4704  sofld  5274  fvmptss  5770  fimacnv  5823  isofr2  6022  frxp  6671  fnse  6678  smores2  6801  f1imaen2g  7358  domunsncan  7399  fissuni  7604  fipreima  7605  dffi3  7669  marypha1lem  7671  ordtypelem7  7726  ordtypelem8  7727  oismo  7742  unxpwdom2  7791  cantnfres  7873  oemapvali  7880  mapfienOLD  7915  tskwe  8108  acndom2  8212  dfac2a  8287  dfac12lem2  8301  cfle  8411  cofsmo  8426  coftr  8430  isf34lem5  8535  isf34lem7  8536  isf34lem6  8537  enfin1ai  8541  fin1a2lem12  8568  ttukeylem7  8672  alephexp1  8731  fpwwe2lem13  8796  fpwwe2  8797  canth4  8801  canthwelem  8804  pwfseqlem1  8812  pwfseqlem4  8816  fzossnn0  11563  limsupgle  12938  limsupgre  12942  rlimres  13019  lo1res  13020  lo1resb  13025  rlimresb  13026  o1resb  13027  o1of2  13073  o1rlimmul  13079  isercolllem2  13126  isercoll  13128  climsup  13130  bitsinvp1  13627  sadcaddlem  13635  sadadd2lem  13637  sadadd3  13639  sadasslem  13648  sadeq  13650  bitsres  13651  smuval2  13660  smupval  13666  smueqlem  13668  smumul  13671  1arith  13970  isstruct2  14165  setscom  14186  ressress  14217  imasvscafn  14457  imasless  14460  mrcssv  14534  isacs1i  14577  mreacs  14578  acsfn  14579  isacs4lem  15320  isacs5lem  15321  mhmima  15472  cntzmhm  15835  f1omvdconj  15931  f1omvdco2  15933  symgsssg  15952  symggen  15955  psgnunilem1  15978  efgval  16193  gsumzaddlem  16387  gsumzaddlemOLD  16389  dmdprdd  16454  dprdfeq0  16485  dprdfeq0OLD  16492  dprdres  16498  dprdss  16499  dprdz  16500  subgdmdprd  16504  dprddisj2  16510  dprddisj2OLD  16511  dprd2dlem1  16513  dprd2da  16514  dprd2d2  16516  dmdprdsplit2lem  16517  lmhmlsp  17051  lsppratlem4  17152  islbs3  17157  lbsextlem3  17162  mplcoe2  17480  mplcoe2OLD  17481  mplind  17515  znleval  17828  evpmss  17857  frlmsslsp  18064  frlmsslspOLD  18065  lindff1  18090  lindfrn  18091  f1lindf  18092  lindfmm  18097  lsslindf  18100  basdif0  18399  tgcl  18415  ppttop  18452  epttop  18454  ntrin  18506  mretopd  18537  neiptoptop  18576  islp3  18591  cnclsi  18717  cnconst2  18728  cnrest  18730  cnrest2  18731  cnpresti  18733  cnprest2  18735  fiuncmp  18848  connsub  18866  conima  18870  iunconlem  18872  1stcfb  18890  2ndc1stc  18896  2ndcdisj  18901  kgentopon  18952  llycmpkgen2  18964  1stckgenlem  18967  kgencn3  18972  ptclsg  19029  ptcnplem  19035  txtube  19054  hausdiag  19059  txkgen  19066  xkoco1cn  19071  xkoco2cn  19072  xkococnlem  19073  qtoptop2  19113  basqtop  19125  imastopn  19134  hmeores  19185  hmphdis  19210  ptcmpfi  19227  fbssfi  19251  filin  19268  infil  19277  fbasrn  19298  fgtr  19304  elfm  19361  imaelfm  19365  hausflim  19395  flimclslem  19398  fclscmp  19444  cnextcn  19480  tmdgsum2  19508  tgpconcomp  19524  tsmsresOLD  19558  ustexsym  19631  ustund  19637  ustimasn  19644  utoptop  19650  utopbas  19651  restutopopn  19654  blin2  19845  metustexhalfOLD  19979  metustexhalf  19980  icccmplem2  20241  icccmplem3  20242  reconnlem2  20245  tchcph  20593  fmcfil  20624  resscdrg  20711  ivthlem2  20777  ivthlem3  20778  ivth2  20780  ovolfiniun  20825  ovoliunlem1  20826  ismbl2  20851  nulmbl2  20859  unmbl  20860  shftmbl  20861  voliunlem1  20872  voliunlem2  20873  ioombl1lem4  20883  uniioombllem4  20907  dyadmbllem  20920  dyadmbl  20921  mbflimsup  20985  i1fima  20997  i1fima2  20998  i1fadd  21014  itg1addlem4  21018  itg2splitlem  21067  itg2split  21068  ellimc3  21195  limcflflem  21196  limcflf  21197  limcresi  21201  limciun  21210  dvreslem  21225  dvres2lem  21226  dvres  21227  dvaddbr  21253  dvmulbr  21254  dvlip  21306  dvlip2  21308  c1liplem1  21309  dvivthlem1  21321  dvne0  21324  lhop1lem  21326  lhop  21329  dvcnvrelem1  21330  dvcnvrelem2  21331  dvfsumle  21334  dvfsumabs  21336  dvfsumlem2  21340  itgsubstlem  21361  mdegleb  21419  mdeglt  21420  mdegldg  21421  mdegxrcl  21422  mdegcl  21424  ig1peu  21527  reeff1olem  21795  logccv  21992  rlimcnp2  22244  ppisval  22325  prmdvdsfi  22329  mumul  22403  sqff1o  22404  chtlepsi  22429  chpub  22443  dchrisum0lem2a  22650  pntlem3  22742  ex-res  23470  ghsubgolem  23679  htthlem  24141  chlejb1i  24701  ssmd2  25538  gsumle  26097  gsumvsca1  26103  gsumvsca2  26104  sibfof  26573  sitgclbn  26576  eulerpartlemgu  26607  ballotlemsima  26745  lgamgulmlem2  26863  erdsze2lem2  26939  iccllyscon  26986  cvmopnlem  27014  relexpdm  27183  relexprn  27184  fprodntriv  27301  nodenselem6  27673  nofulllem5  27693  cnambfre  28281  itg2gt0cn  28288  neiin  28368  neibastop1  28421  neibastop2lem  28422  topmeet  28426  sstotbnd2  28514  sstotbnd3  28516  ssbnd  28528  ismtyima  28543  heibor1lem  28549  isnacs2  28884  isnacs3  28888  diophrw  28939  pellfundre  29064  pellfundge  29065  pellfundlb  29067  pellfundglb  29068  fnwe2lem2  29246  lmhmfgima  29279  hbt  29328  climinf  29622  stoweidlem27  29665  bnj1311  31714  pmodlem2  33061  pmodN  33064  diaintclN  34273  djaclN  34351  dibintclN  34382  dicval  34391  dihoml4c  34591  djhcl  34615
  Copyright terms: Public domain W3C validator