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

Theorem syl6ss 3277
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl6ss.1  |-  ( ph  ->  A  C_  B )
syl6ss.2  |-  B  C_  C
Assertion
Ref Expression
syl6ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl6ss
StepHypRef Expression
1 syl6ss.1 . 2  |-  ( ph  ->  A  C_  B )
2 syl6ss.2 . . 3  |-  B  C_  C
32a1i 10 . 2  |-  ( ph  ->  B  C_  C )
41, 3sstrd 3275 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3238
This theorem is referenced by:  difss2  3392  rintn0  4094  ssxpb  5213  relfld  5301  coexg  5318  funssxp  5508  dff2  5783  dff3  5784  fliftf  5937  1stcof  6274  2ndcof  6275  oacomf1olem  6704  nnunifi  7255  elfiun  7330  marypha1lem  7333  marypha1  7334  ordtypelem7  7386  tcmin  7573  unwf  7629  tcrank  7701  numacn  7823  aceq3lem  7894  dfac12lem2  7917  ackbij1lem9  8001  ackbij1lem10  8002  ackbij1lem16  8008  fin23lem26  8098  fin23lem27  8101  fin1a2lem6  8178  itunitc  8194  axdc3lem2  8224  ttukeylem5  8287  fpwwe2lem13  8411  canthwelem  8419  pwfseqlem4  8431  wunex2  8507  wunex3  8510  inar1  8544  inatsk  8547  gruina  8587  suprzub  10460  uzsupss  10461  uzwo3  10462  rpnnen1lem4  10496  rpnnen1lem5  10497  supxrre  10799  infmxrre  10807  ioodisj  10918  injresinjlem  11086  uzindi  11207  seqcoll  11599  seqcoll2  11600  limsupval2  12161  limsupgre  12162  limsupbnd2  12164  rlimuni  12231  rlimcld2  12259  rlimno1  12334  isercolllem2  12346  isercoll  12348  summolem2a  12396  summolem2  12397  fsumsers  12409  fsumcvg3  12410  4sqlem11  13210  vdwlem8  13243  vdwlem11  13246  ramub2  13269  0ram  13275  0ram2  13276  0ramcl  13278  ramub1lem1  13281  ramub1lem2  13282  isohom  13884  funcres2c  13985  resscntz  15017  cntzidss  15023  cntzmhm2  15025  pgpssslw  15135  cntzspan  15347  gsumval3  15401  gsum2d  15433  dprdspan  15472  dpjidcl  15503  lssintcl  15931  lbsextlem2  16122  lbsextlem3  16123  lbsextlem4  16124  mplbas2  16422  fctop  16958  cctop  16960  clsval2  17004  ordtbas2  17138  ordtopn1  17141  ordtopn2  17142  lmss  17243  clscon  17373  2ndcdisj  17399  2ndcomap  17401  llycmpkgen2  17462  1stckgen  17466  ptbasfi  17493  txcmplem2  17553  hausdiag  17556  txkgen  17563  basqtop  17619  alexsublem  17951  alexsubb  17953  alexsubALTlem4  17957  tsmsres  18039  tsmsxplem1  18048  tsmsxp  18050  prdsmet  18147  icccmplem2  18542  xrge0tsms  18553  cnmptre  18640  icchmeo  18654  bndth  18671  lebnumlem2  18675  cfilresi  18936  causs  18939  bcthlem3  18963  bcthlem5  18965  evthicc  19034  ovolficcss  19044  ovolmge0  19051  ovolgelb  19054  ovollb2lem  19062  ovollb2  19063  ovolunlem1a  19070  ovolunlem1  19071  ovoliunlem1  19076  ovoliunlem2  19077  ovoliun  19079  ovolscalem1  19087  ovolicc1  19090  ovolicc2lem4  19094  ovolicc2  19096  voliunlem2  19123  voliunlem3  19124  ioombl1lem2  19131  ioombl1lem4  19133  uniioovol  19149  uniiccvol  19150  uniioombllem1  19151  uniioombllem2  19153  uniioombllem3  19155  uniioombllem4  19156  uniioombllem6  19158  dyadmbllem  19169  dyadmbl  19170  volcn  19176  vitalilem4  19181  vitalilem5  19182  cnmbf  19229  i1fmul  19266  itg1addlem4  19269  itg2seq  19312  dvbssntr  19465  dvreslem  19474  dvcjbr  19513  dvferm1  19547  dvferm2  19549  cmvth  19553  dvlip  19555  lhop1lem  19575  lhop2  19577  lhop  19578  dvcnvrelem2  19580  dvcnvre  19581  dvfsumle  19583  dvfsumge  19584  dvfsumabs  19585  dvfsumlem2  19589  ftc1a  19599  ftc1lem3  19600  ftc1lem6  19603  itgsubstlem  19610  mdegleb  19665  mdeglt  19666  mdegldg  19667  mdegxrcl  19668  mdegcl  19670  deg1mul3le  19717  ig1pdvds  19777  plyeq0lem  19807  aannenlem2  19924  aalioulem3  19929  taylf  19955  taylthlem2  19968  pserulm  20016  psercn2  20017  psercn  20020  reeff1olem  20040  efcvx  20043  loglesqr  20320  rlimcnp  20482  xrlimcnp  20485  jensen  20505  wilthlem2  20530  vmadivsumb  20855  pntrsumo1  20937  pntlem3  20981  nmoxr  21657  nmooge0  21658  nmoolb  21662  nmoubi  21663  ubthlem1  21762  shmodi  22282  nmopxr  22759  nmfnxr  22772  nmoplb  22800  nmopub  22801  nmfnlb  22817  nmfnleub  22818  nmopun  22907  branmfn  22998  mdslj1i  23212  hatomistici  23255  eqbrrdva  23431  suppss2f  23452  xppreima2  23462  fzssnn  23548  xrge0tsmsd  23614  ustrel  23716  metustrel  23795  sigaclci  23980  insiga  23985  ballotlemsima  24221  rescon  24380  cvmliftlem8  24426  cvmlift3lem6  24458  prodmolem2a  24744  prodmolem2  24745  zprod  24747  nofulllem5  25101  axcontlem10  25343  itg2gt0cn  25678  ftc1cnnc  25697  areacirclem4  25702  areacirclem1  25703  areacirclem5  25704  ivthALT  25765  neibastop1  25815  neibastop2lem  25816  topjoin  25821  totbndbnd  26019  prdsbnd  26023  heiborlem1  26041  rrnequiv  26065  reheibor  26069  iccbnd  26070  eldioph2lem2  26346  rmxyelqirr  26501  ttac  26635  islinds3  26810  hbtlem6  26839  hbt  26840  ibliccsinexp  27251  iblioosinexp  27253  usgraexmpl  27585  bnj1145  28787  bnj1137  28789  bnj1136  28791  pmapssbaN  30020  2polssN  30175  paddunN  30187  poldmj1N  30188  ispsubcl2N  30207  psubclinN  30208  paddatclN  30209  poml4N  30213  diaglbN  31316  diaintclN  31319  dibglbN  31427  dibintclN  31428  dicssdvh  31447  dihvalrel  31540  dochexmidlem4  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator