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

Theorem syl5ss 3515
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 3514 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  wereu2  4876  sofld  5453  fvmptss  5956  fimacnv  6011  isofr2  6226  frxp  6890  fnse  6897  smores2  7022  f1imaen2g  7573  domunsncan  7614  fissuni  7821  fipreima  7822  dffi3  7887  marypha1lem  7889  ordtypelem7  7945  ordtypelem8  7946  oismo  7961  unxpwdom2  8010  cantnfres  8092  oemapvali  8099  mapfienOLD  8134  tskwe  8327  acndom2  8431  dfac2a  8506  dfac12lem2  8520  cfle  8630  cofsmo  8645  coftr  8649  isf34lem5  8754  isf34lem7  8755  isf34lem6  8756  enfin1ai  8760  fin1a2lem12  8787  ttukeylem7  8891  alephexp1  8950  fpwwe2lem13  9016  fpwwe2  9017  canth4  9021  canthwelem  9024  pwfseqlem1  9032  pwfseqlem4  9036  fzossnn0  11820  fsuppmapnn0fiublem  12060  fsuppmapnn0fiub  12061  limsupgle  13259  limsupgre  13263  rlimres  13340  lo1res  13341  lo1resb  13346  rlimresb  13347  o1resb  13348  o1of2  13394  o1rlimmul  13400  isercolllem2  13447  isercoll  13449  climsup  13451  bitsinvp1  13954  sadcaddlem  13962  sadadd2lem  13964  sadadd3  13966  sadasslem  13975  sadeq  13977  bitsres  13978  smuval2  13987  smupval  13993  smueqlem  13995  smumul  13998  1arith  14300  isstruct2  14495  setscom  14516  ressress  14548  imasvscafn  14788  imasless  14791  mrcssv  14865  isacs1i  14908  mreacs  14909  acsfn  14910  isacs4lem  15651  isacs5lem  15652  mhmima  15804  cntzmhm  16171  f1omvdconj  16267  f1omvdco2  16269  symgsssg  16288  symggen  16291  psgnunilem1  16314  efgval  16531  gsumzaddlem  16725  gsumzaddlemOLD  16727  dmdprdd  16821  dprdfeq0  16852  dprdfeq0OLD  16859  dprdres  16865  dprdss  16866  dprdz  16867  subgdmdprd  16871  dprddisj2  16877  dprddisj2OLD  16878  dprd2dlem1  16880  dprd2da  16881  dprd2d2  16883  dmdprdsplit2lem  16884  lmhmlsp  17478  lsppratlem4  17579  islbs3  17584  lbsextlem3  17589  mplcoe5  17902  mplcoe2OLD  17904  mplind  17938  znleval  18360  evpmss  18389  frlmsslsp  18596  frlmsslspOLD  18597  lindff1  18622  lindfrn  18623  f1lindf  18624  lindfmm  18629  lsslindf  18632  basdif0  19221  tgcl  19237  ppttop  19274  epttop  19276  ntrin  19328  mretopd  19359  neiptoptop  19398  islp3  19413  cnclsi  19539  cnconst2  19550  cnrest  19552  cnrest2  19553  cnpresti  19555  cnprest2  19557  fiuncmp  19670  connsub  19688  conima  19692  iunconlem  19694  1stcfb  19712  2ndc1stc  19718  2ndcdisj  19723  kgentopon  19774  llycmpkgen2  19786  1stckgenlem  19789  kgencn3  19794  ptclsg  19851  ptcnplem  19857  txtube  19876  hausdiag  19881  txkgen  19888  xkoco1cn  19893  xkoco2cn  19894  xkococnlem  19895  qtoptop2  19935  basqtop  19947  imastopn  19956  hmeores  20007  hmphdis  20032  ptcmpfi  20049  fbssfi  20073  filin  20090  infil  20099  fbasrn  20120  fgtr  20126  elfm  20183  imaelfm  20187  hausflim  20217  flimclslem  20220  fclscmp  20266  cnextcn  20302  tmdgsum2  20330  tgpconcomp  20346  tsmsresOLD  20380  ustexsym  20453  ustund  20459  ustimasn  20466  utoptop  20472  utopbas  20473  restutopopn  20476  blin2  20667  metustexhalfOLD  20801  metustexhalf  20802  icccmplem2  21063  icccmplem3  21064  reconnlem2  21067  tchcph  21415  fmcfil  21446  resscdrg  21533  ivthlem2  21599  ivthlem3  21600  ivth2  21602  ovolfiniun  21647  ovoliunlem1  21648  ismbl2  21673  nulmbl2  21682  unmbl  21683  shftmbl  21684  voliunlem1  21695  voliunlem2  21696  ioombl1lem4  21706  uniioombllem4  21730  dyadmbllem  21743  dyadmbl  21744  mbflimsup  21808  i1fima  21820  i1fima2  21821  i1fadd  21837  itg1addlem4  21841  itg2splitlem  21890  itg2split  21891  ellimc3  22018  limcflflem  22019  limcflf  22020  limcresi  22024  limciun  22033  dvreslem  22048  dvres2lem  22049  dvres  22050  dvaddbr  22076  dvmulbr  22077  dvlip  22129  dvlip2  22131  c1liplem1  22132  dvivthlem1  22144  dvne0  22147  lhop1lem  22149  lhop  22152  dvcnvrelem1  22153  dvcnvrelem2  22154  dvfsumle  22157  dvfsumabs  22159  dvfsumlem2  22163  itgsubstlem  22184  mdegleb  22199  mdeglt  22200  mdegldg  22201  mdegxrcl  22202  mdegcl  22204  ig1peu  22307  reeff1olem  22575  logccv  22772  rlimcnp2  23024  ppisval  23105  prmdvdsfi  23109  mumul  23183  sqff1o  23184  chtlepsi  23209  chpub  23223  dchrisum0lem2a  23430  pntlem3  23522  ex-res  24839  ghsubgolem  25048  htthlem  25510  chlejb1i  26070  ssmd2  26907  gsumle  27433  sibfof  27922  sitgclbn  27925  eulerpartlemgu  27956  ballotlemsima  28094  lgamgulmlem2  28212  erdsze2lem2  28288  iccllyscon  28335  cvmopnlem  28363  relexpdm  28533  relexprn  28534  fprodntriv  28651  nodenselem6  29023  nofulllem5  29043  cnambfre  29640  itg2gt0cn  29647  neiin  29727  neibastop1  29780  neibastop2lem  29781  topmeet  29785  sstotbnd2  29873  sstotbnd3  29875  ssbnd  29887  ismtyima  29902  heibor1lem  29908  isnacs2  30242  isnacs3  30246  diophrw  30296  pellfundre  30421  pellfundge  30422  pellfundlb  30424  pellfundglb  30425  fnwe2lem2  30601  lmhmfgima  30634  hbt  30683  climinf  31148  limccog  31162  limcleqr  31186  itgcoscmulx  31287  stoweidlem27  31327  dirkercncflem2  31404  fourierdlem49  31456  fourierdlem54  31461  fourierdlem62  31469  fourierdlem68  31475  fourierdlem101  31508  fourierdlem111  31518  bnj1311  33159  pmodlem2  34643  pmodN  34646  diaintclN  35855  djaclN  35933  dibintclN  35964  dicval  35973  dihoml4c  36173  djhcl  36197  xptrrel  36785  rp-imass  36796
  Copyright terms: Public domain W3C validator