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

Theorem syl5ss 3359
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 3358 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3320
This theorem is referenced by:  wereu2  4579  sofld  5318  fvmptss  5813  fimacnv  5862  isofr2  6064  frxp  6456  fnse  6463  smores2  6616  f1imaen2g  7168  domunsncan  7208  fissuni  7411  fipreima  7412  dffi3  7436  marypha1lem  7438  ordtypelem7  7493  ordtypelem8  7494  oismo  7509  unxpwdom2  7556  oemapvali  7640  mapfien  7653  tskwe  7837  acndom2  7935  dfac2a  8010  dfac12lem2  8024  cfle  8134  cofsmo  8149  coftr  8153  isf34lem5  8258  isf34lem7  8259  isf34lem6  8260  enfin1ai  8264  fin1a2lem12  8291  ttukeylem7  8395  alephexp1  8454  fpwwe2lem13  8517  fpwwe2  8518  canth4  8522  canthwelem  8525  pwfseqlem1  8533  pwfseqlem4  8537  limsupgle  12271  limsupgre  12275  rlimres  12352  lo1res  12353  lo1resb  12358  rlimresb  12359  o1resb  12360  o1of2  12406  o1rlimmul  12412  isercolllem2  12459  isercoll  12461  climsup  12463  bitsinvp1  12961  sadcaddlem  12969  sadadd2lem  12971  sadadd3  12973  sadasslem  12982  sadeq  12984  bitsres  12985  smuval2  12994  smupval  13000  smueqlem  13002  smumul  13005  1arith  13295  isstruct2  13478  setscom  13497  ressress  13526  imasvscafn  13762  imasless  13765  mrcssv  13839  isacs1i  13882  mreacs  13883  acsfn  13884  isacs4lem  14594  isacs5lem  14595  mhmima  14763  cntzmhm  15137  efgval  15349  gsumzaddlem  15526  dmdprdd  15560  dprdfeq0  15580  dprdres  15586  dprdss  15587  dprdz  15588  subgdmdprd  15592  dprddisj2  15597  dprd2dlem1  15599  dprd2da  15600  dprd2d2  15602  dmdprdsplit2lem  15603  lmhmlsp  16125  lsppratlem4  16222  islbs3  16227  lbsextlem3  16232  mplcoe2  16530  mplind  16562  znleval  16835  basdif0  17018  tgcl  17034  ppttop  17071  epttop  17073  ntrin  17125  mretopd  17156  neiptoptop  17195  islp3  17210  cnclsi  17336  cnconst2  17347  cnrest  17349  cnrest2  17350  cnpresti  17352  cnprest2  17354  fiuncmp  17467  connsub  17484  conima  17488  iunconlem  17490  1stcfb  17508  2ndc1stc  17514  2ndcdisj  17519  kgentopon  17570  llycmpkgen2  17582  1stckgenlem  17585  kgencn3  17590  ptclsg  17647  ptcnplem  17653  txtube  17672  hausdiag  17677  txkgen  17684  xkoco1cn  17689  xkoco2cn  17690  xkococnlem  17691  qtoptop2  17731  basqtop  17743  imastopn  17752  hmeores  17803  hmphdis  17828  ptcmpfi  17845  fbssfi  17869  filin  17886  infil  17895  fbasrn  17916  fgtr  17922  elfm  17979  imaelfm  17983  hausflim  18013  flimclslem  18016  fclscmp  18062  cnextcn  18098  tmdgsum2  18126  tgpconcomp  18142  tsmsres  18173  ustexsym  18245  ustund  18251  ustimasn  18258  utoptop  18264  utopbas  18265  restutopopn  18268  blin2  18459  metustexhalfOLD  18593  metustexhalf  18594  icccmplem2  18854  icccmplem3  18855  reconnlem2  18858  tchcph  19194  fmcfil  19225  resscdrg  19312  ivthlem2  19349  ivthlem3  19350  ivth2  19352  ovolfiniun  19397  ovoliunlem1  19398  ismbl2  19423  nulmbl2  19431  unmbl  19432  shftmbl  19433  voliunlem1  19444  voliunlem2  19445  ioombl1lem4  19455  uniioombllem4  19478  dyadmbllem  19491  dyadmbl  19492  mbflimsup  19558  i1fima  19570  i1fima2  19571  i1fadd  19587  itg1addlem4  19591  itg2splitlem  19640  itg2split  19641  ellimc3  19766  limcflflem  19767  limcflf  19768  limcresi  19772  limciun  19781  dvreslem  19796  dvres2lem  19797  dvres  19798  dvaddbr  19824  dvmulbr  19825  dvlip  19877  dvlip2  19879  c1liplem1  19880  dvivthlem1  19892  dvne0  19895  lhop1lem  19897  lhop  19900  dvcnvrelem1  19901  dvcnvrelem2  19902  dvfsumle  19905  dvfsumabs  19907  dvfsumlem2  19911  itgsubstlem  19932  mdegleb  19987  mdeglt  19988  mdegldg  19989  mdegxrcl  19990  mdegcl  19992  ig1peu  20094  reeff1olem  20362  logccv  20554  rlimcnp2  20805  ppisval  20886  prmdvdsfi  20890  mumul  20964  sqff1o  20965  chtlepsi  20990  chpub  21004  dchrisum0lem2a  21211  pntlem3  21303  ex-res  21749  ghsubgolem  21958  htthlem  22420  chlejb1i  22978  ssmd2  23815  sibfof  24654  sitgclbn  24657  ballotlemsima  24773  lgamgulmlem2  24814  erdsze2lem2  24890  iccllyscon  24937  cvmopnlem  24965  relexpdm  25135  relexprn  25136  fprodntriv  25268  nodenselem6  25641  nofulllem5  25661  cnambfre  26255  itg2gt0cn  26260  neiin  26335  neibastop1  26388  neibastop2lem  26389  topmeet  26393  sstotbnd2  26483  sstotbnd3  26485  ssbnd  26497  ismtyima  26512  heibor1lem  26518  isnacs2  26760  isnacs3  26764  diophrw  26817  pellfundre  26944  pellfundge  26945  pellfundlb  26947  pellfundglb  26948  fnwe2lem2  27126  lmhmfgima  27159  frlmsslsp  27225  lindff1  27267  lindfrn  27268  f1lindf  27269  lindfmm  27274  lsslindf  27277  hbt  27311  f1omvdconj  27366  f1omvdco2  27368  symgsssg  27385  symggen  27388  psgnunilem1  27393  climinf  27708  stoweidlem27  27752  fzossnn0  28124  bnj1311  29393  pmodlem2  30644  pmodN  30647  diaintclN  31856  djaclN  31934  dibintclN  31965  dicval  31974  dihoml4c  32174  djhcl  32198
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator