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

Theorem syl6ss 3328
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 11 . 2  |-  ( ph  ->  B  C_  C )
41, 3sstrd 3326 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3288
This theorem is referenced by:  difss2  3444  rintn0  4149  eqbrrdva  5009  ssxpb  5270  relfld  5362  funssxp  5571  dff2  5848  dff3  5849  fliftf  6004  1stcof  6341  2ndcof  6342  nnunifi  7325  elfiun  7401  marypha1lem  7404  marypha1  7405  ordtypelem7  7457  tcmin  7644  unwf  7700  tcrank  7772  aceq3lem  7965  dfac12lem2  7988  ackbij1lem9  8072  ackbij1lem10  8073  ackbij1lem16  8079  fin23lem26  8169  fin23lem27  8172  fin1a2lem6  8249  itunitc  8265  axdc3lem2  8295  ttukeylem5  8357  fpwwe2lem13  8481  canthwelem  8489  pwfseqlem4  8501  wunex2  8577  wunex3  8580  inar1  8614  inatsk  8617  gruina  8657  suprzub  10531  uzsupss  10532  uzwo3  10533  rpnnen1lem4  10567  rpnnen1lem5  10568  supxrre  10870  infmxrre  10878  ioodisj  10990  injresinjlem  11162  uzindi  11283  seqcoll  11675  seqcoll2  11676  limsupval2  12237  limsupgre  12238  limsupbnd2  12240  rlimuni  12307  rlimcld2  12335  rlimno1  12410  isercolllem2  12422  isercoll  12424  summolem2a  12472  summolem2  12473  fsumsers  12485  fsumcvg3  12486  4sqlem11  13286  vdwlem8  13319  vdwlem11  13322  ramub2  13345  0ram  13351  0ram2  13352  0ramcl  13354  ramub1lem2  13358  isohom  13960  funcres2c  14061  resscntz  15093  cntzidss  15099  cntzmhm2  15101  pgpssslw  15211  cntzspan  15423  gsumval3  15477  gsum2d  15509  dprdspan  15548  lssintcl  16003  lbsextlem2  16194  lbsextlem3  16195  lbsextlem4  16196  mplbas2  16494  fctop  17031  cctop  17033  neitr  17206  ordtbas2  17217  ordtopn1  17220  ordtopn2  17221  lmss  17324  clscon  17454  2ndcdisj  17480  2ndcomap  17482  ptbasfi  17574  txcmplem2  17635  hausdiag  17638  txkgen  17645  basqtop  17704  alexsubb  18038  alexsubALTlem4  18042  tsmsres  18134  tsmsxplem1  18143  tsmsxp  18145  ustrel  18202  utop3cls  18242  prdsmet  18361  metustrelOLD  18546  metustrel  18547  icccmplem2  18815  xrge0tsms  18826  cnmptre  18913  icchmeo  18927  bndth  18944  lebnumlem2  18948  cfilresi  19209  causs  19212  bcthlem5  19242  evthicc  19317  ovolficcss  19327  ovolmge0  19334  ovolgelb  19337  ovollb2lem  19345  ovollb2  19346  ovolunlem1a  19353  ovolunlem1  19354  ovoliunlem1  19359  ovoliunlem2  19360  ovoliun  19362  ovolscalem1  19370  ovolicc1  19373  ovolicc2lem4  19377  ovolicc2  19379  voliunlem2  19406  voliunlem3  19407  ioombl1lem2  19414  ioombl1lem4  19416  uniioovol  19432  uniiccvol  19433  uniioombllem1  19434  uniioombllem2  19436  uniioombllem3  19438  uniioombllem4  19439  uniioombllem6  19441  dyadmbllem  19452  dyadmbl  19453  volcn  19459  vitalilem4  19464  vitalilem5  19465  cnmbf  19512  i1fmul  19549  itg1addlem4  19552  itg2seq  19595  dvbssntr  19748  dvreslem  19757  dvcjbr  19796  dvferm1  19830  dvferm2  19832  cmvth  19836  dvlip  19838  lhop1lem  19858  lhop2  19860  lhop  19861  dvcnvrelem2  19863  dvcnvre  19864  dvfsumle  19866  dvfsumge  19867  dvfsumabs  19868  dvfsumlem2  19872  ftc1a  19882  ftc1lem3  19883  ftc1lem6  19886  itgsubstlem  19893  mdegleb  19948  mdeglt  19949  mdegldg  19950  mdegxrcl  19951  mdegcl  19953  deg1mul3le  20000  ig1pdvds  20060  plyeq0lem  20090  aannenlem2  20207  aalioulem3  20212  taylf  20238  taylthlem2  20251  pserulm  20299  psercn2  20300  psercn  20303  reeff1olem  20323  efcvx  20326  loglesqr  20603  rlimcnp  20765  xrlimcnp  20768  jensen  20788  wilthlem2  20813  vmadivsumb  21138  pntrsumo1  21220  pntlem3  21264  usgraexmpl  21381  nmoxr  22228  nmooge0  22229  nmoolb  22233  nmoubi  22234  ubthlem1  22333  shmodi  22853  nmopxr  23330  nmfnxr  23343  nmoplb  23371  nmopub  23372  nmfnlb  23388  nmfnleub  23389  nmopun  23478  branmfn  23569  mdslj1i  23783  hatomistici  23826  suppss2f  24010  xppreima2  24021  fzssnn  24108  xrge0tsmsd  24184  metideq  24249  metider  24250  pstmfval  24252  sigaclci  24476  insiga  24481  ballotlemsima  24734  rescon  24894  cvmliftlem8  24940  cvmlift3lem6  24972  prodmolem2a  25221  prodmolem2  25222  zprod  25224  nofulllem5  25582  axcontlem10  25824  mblfinlem  26151  mblfinlem2  26152  mblfinlem3  26153  ismblfin  26154  itg2gt0cn  26167  ftc1cnnc  26186  areacirclem4  26191  areacirclem1  26192  areacirclem5  26193  ivthALT  26236  neibastop1  26286  topjoin  26292  totbndbnd  26396  prdsbnd  26400  heiborlem1  26418  rrnequiv  26442  reheibor  26446  iccbnd  26447  rmxyelqirr  26871  ttac  27005  islinds3  27180  hbtlem6  27209  hbt  27210  ibliccsinexp  27620  iblioosinexp  27622  stoweidlem34  27658  stoweidlem59  27683  swrdccatin12  28034  bnj1145  29080  bnj1137  29082  bnj1136  29084  pmapssbaN  30254  2polssN  30409  paddunN  30421  poldmj1N  30422  ispsubcl2N  30441  psubclinN  30442  paddatclN  30443  poml4N  30447  diaglbN  31550  diaintclN  31553  dibglbN  31661  dibintclN  31662  dicssdvh  31681  dihvalrel  31774  dochexmidlem4  31958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator