Theorem sstrd 3613

Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)

Hypotheses

Ref	Expression
sstrd.1	|- ( ph -> A C_ B )
sstrd.2	|- ( ph -> B C_ C )

Assertion

Ref	Expression
sstrd	|- ( ph -> A C_ C )

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstrd.1	. 2 |- ( ph -> A C_ B )
2		sstrd.2	. 2 |- ( ph -> B C_ C )
3		sstr 3611	. 2 |- ( ( A C_ B /\ B C_ C ) -> A C_ C )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  syl5ss  3614  syl6ss  3615  ssdif2d  3749  uniintsn  4514  funss  5907  fssxp  6060  fimass  6081  knatar  6607  tfisi  7058  suppfnss  7320  suppssov1  7327  suppssfv  7331  tposss  7353  tfrlem1  7472  omwordri  7652  oewordri  7672  oeeui  7682  oaabs2  7725  omopthlem1  7735  ecinxp  7822  sbthlem1  8070  dffi2  8329  hartogslem1  8447  cantnfcl  8564  cantnflt  8569  cantnfp1lem3  8577  cantnflem3  8588  cnfcom  8597  cnfcom3lem  8600  rankssb  8711  tskwe  8776  dfac12lem2  8966  dfac12lem3  8967  cfflb  9081  cfcof  9096  ssfin2  9142  hsmexlem4  9251  ttukeylem6  9336  ttukeylem7  9337  fpwwe2lem1  9453  fpwwe2lem8  9459  fpwwe2lem11  9462  fpwwe2lem12  9463  canthnumlem  9470  canthwelem  9472  canthwe  9473  canthp1lem2  9475  pwfseqlem5  9485  wunex2  9560  tsktrss  9583  inttsk  9596  uzwo3  11783  supicc  12320  supiccub  12321  supicclub  12322  ssfzunsnext  12386  seqsplit  12834  seqf1olem2a  12839  seqz  12849  swrdval2  13420  trrelssd  13712  rtrclreclem4  13801  sumss  14455  qshash  14559  incexc  14569  incexc2  14570  prodss  14677  rpnnen2lem11  14953  vdwlem1  15685  ramub1lem1  15730  imasaddvallem  16189  imasvscaf  16199  mrerintcl  16257  ismred2  16263  mremre  16264  mrcuni  16281  mressmrcd  16287  submrc  16288  mrissmrid  16301  mreexexlem2d  16305  isacs2  16314  isacs1i  16318  invss  16421  ssctr  16485  funcres2b  16557  isacs3lem  17166  acsfiindd  17177  acsmapd  17178  acsmap2d  17179  tsrdir  17238  subsubm  17357  gsumwspan  17383  subsubg  17617  subgint  17618  cntzidss  17770  symggen  17890  pmtrdifellem1  17896  pmtrdifellem2  17897  pgpssslw  18029  lsmless1x  18059  lsmless2x  18060  lsmless12  18076  subglsm  18086  gsumval3lem2  18307  gsumzaddlem  18321  gsumzadd  18322  gsum2d  18371  dmdprdd  18398  dprdfeq0  18421  dprdspan  18426  dprdres  18427  dprdss  18428  dprdz  18429  subgdmdprd  18433  subgdprd  18434  dprdsn  18435  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  dprdsplit  18447  pgpfac1lem2  18474  pgpfac1lem3  18476  pgpfac1lem5  18478  subsubrg  18806  lspss  18984  lspun  18987  lsslsp  19015  lmhmlsp  19049  lsmelval2  19085  lsmssspx  19088  lsppratlem2  19148  lsppratlem3  19149  lsppratlem4  19150  lbsextlem2  19159  lbsextlem3  19160  aspss  19332  ocvlsp  20020  cssmre  20037  obselocv  20072  obslbs  20074  toponmre  20897  neiint  20908  neiss  20913  lpss  20946  lpss3  20948  restopnb  20979  restfpw  20983  neitr  20984  restcls  20985  restntr  20986  restlp  20987  ordtbas  20996  pnfnei  21024  mnfnei  21025  iscnp4  21067  cnclsi  21076  isreg2  21181  discmp  21201  cmpcld  21205  uncmp  21206  sscmp  21208  hauscmplem  21209  cmpfi  21211  iunconnlem  21230  clsconn  21233  2ndcctbss  21258  restnlly  21285  llyrest  21288  nllyrest  21289  llyidm  21291  nllyidm  21292  cldllycmp  21298  dislly  21300  comppfsc  21335  llycmpkgen2  21353  ptbasfi  21384  txnlly  21440  txcmplem1  21444  tx1stc  21453  xkococnlem  21462  qtopval2  21499  basqtop  21514  tgqtop  21515  qtoprest  21520  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  fsubbas  21671  fgabs  21683  fbasrn  21688  trfil2  21691  trfg  21695  isufil2  21712  trufil  21714  ssufl  21722  ufileu  21723  filufint  21724  fmfnfmlem4  21761  fmfnfm  21762  flimss2  21776  flimss1  21777  fclsfnflim  21831  flimfnfcls  21832  fclscmp  21834  cnpfcfi  21844  alexsubALT  21855  clssubg  21912  clsnsg  21913  tsmsres  21947  ustexsym  22019  ustex2sym  22020  ustex3sym  22021  ustund  22025  ustneism  22027  trust  22033  utoptop  22038  restutopopn  22042  utop2nei  22054  utopreg  22056  cfiluweak  22099  neipcfilu  22100  blssps  22229  blss  22230  blcld  22310  blsscls  22312  met1stc  22326  met2ndci  22327  metust  22363  cfilucfil  22364  restmetu  22375  tgqioo  22603  xrsblre  22614  reconnlem2  22630  xrge0gsumle  22636  xrge0tsms  22637  rescncf  22700  cnmpt2pc  22727  cnheibor  22754  cnllycmp  22755  lebnum  22763  phtpycn  22782  cfilfcls  23072  iscmet3lem2  23090  cmetss  23113  cncmet  23119  bcthlem4  23124  bcth3  23128  rrxcph  23180  rrxmetlem  23190  minveclem4a  23201  minveclem4  23203  ivthicc  23227  ovollb  23247  ovollb2lem  23256  ovollb2  23257  nulmbl2  23304  ioorcl2  23340  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  opnmbllem  23369  volcn  23374  volivth  23375  mbfeqalem  23409  itg10a  23477  mbfi1fseqlem4  23485  ditgcl  23622  ditgswap  23623  ditgsplitlem  23624  limcflf  23645  limcres  23650  dvbss  23665  dvbsss  23666  perfdvf  23667  dvreslem  23673  dvres2lem  23674  dvres3  23677  dvcnp  23682  dvcnp2  23683  dvcn  23684  dvnff  23686  dvn2bss  23693  dvnres  23694  cpnord  23698  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvnfre  23715  dvmptres2  23725  dvmptntr  23734  dvcnvlem  23739  dvcnv  23740  dvferm1lem  23747  dvferm2lem  23749  dvlip  23756  dvlipcn  23757  dvlip2  23758  c1liplem1  23759  dvgt0lem1  23765  lhop1lem  23776  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  ftc1lem1  23798  ftc1lem2  23799  ftc1a  23800  ftc1lem4  23802  ftc2ditglem  23808  itgsubstlem  23811  ig1peu  23931  ig1pdvds  23936  taylfvallem1  24111  tayl0  24116  taylply2  24122  taylply  24123  dvtaylp  24124  dvntaylp  24125  dvntaylp0  24126  taylthlem1  24127  ulmdvlem1  24154  ulmdvlem3  24156  psercn  24180  pserdvlem2  24182  abelth  24195  xrlimcnp  24695  lgamucov  24764  wilthlem2  24795  sqff1o  24908  chtublem  24936  pntlemq  25290  pntlemf  25294  tglineintmo  25537  ttgcontlem1  25765  pthdlem1  26662  shintcli  28188  shub1  28241  mdslmd1lem1  29184  mdexchi  29194  chirredlem1  29249  mdsymlem5  29266  sumdmdii  29274  sumdmdlem2  29278  xrsupssd  29524  xrge0infssd  29526  xrge0tsmsd  29785  smatrcl  29862  locfinreflem  29907  cmpcref  29917  pnfneige0  29997  esum2d  30155  insiga  30200  sssigagen2  30209  dynkin  30230  dya2iocnei  30344  omsmon  30360  carsgclctunlem1  30379  carsggect  30380  omsmeas  30385  ftc2re  30676  fdvneggt  30678  fdvnegge  30680  reprsuc  30693  reprss  30695  reprlt  30697  reprinfz1  30700  logdivsqrle  30728  hgt750lemb  30734  bnj906  31000  bnj1020  31033  bnj1137  31063  bnj1408  31104  bnj1452  31120  erdszelem7  31179  erdszelem8  31180  erdsze2lem1  31185  connpconn  31217  cvmliftmolem1  31263  cvmlift2lem1  31284  cvmlift2lem9  31293  cvmlift2lem10  31294  cvmlift3lem6  31306  cvmlift3lem7  31307  ss2mcls  31465  dftrpred3g  31733  sssslt1  31906  sssslt2  31907  scutbdaybnd  31921  neibastop2lem  32355  fnemeet2  32362  fnejoin1  32363  ontgval  32430  unbdqndv1  32499  opnmbllem0  33445  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  sstotbnd2  33573  heiborlem1  33610  heiborlem8  33617  intidl  33828  lsmsat  34295  lssats  34299  lpssat  34300  lssatle  34302  lssat  34303  lsatcvatlem  34336  paddss12  35105  paddasslem17  35122  pmodlem1  35132  pmod1i  35134  pmodl42N  35137  elpcliN  35179  pclfinN  35186  polcon3N  35203  polcon2N  35205  paddunN  35213  pclfinclN  35236  poml5N  35240  osumcllem1N  35242  osumcllem2N  35243  osumcllem3N  35244  pl42lem2N  35266  pl42lem4N  35268  cdlemn5pre  36489  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord5b  36548  dochss  36654  dochdmj1  36679  djhsumss  36696  djhunssN  36698  dochexmidlem2  36750  lclkrslem1  36826  lclkrslem2  36827  lcfrlem2  36832  elrfi  37257  ismrcd1  37261  istopclsd  37263  mrefg2  37270  aomclem2  37625  aomclem6  37629  hbtlem6  37699  hbt  37700  mptrcllem  37920  dfrcl2  37966  relexp0a  38008  trclimalb2  38018  frege81d  38039  k0004ss2  38450  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  uzwo4  39221  ssin0  39223  ixpssmapc  39243  ssinc  39264  ssdec  39265  supxrre3  39541  uzfissfz  39542  ssuzfz  39565  ssrexr  39659  supminfxr  39694  inficc  39761  ressiocsup  39781  ressioosup  39782  ressiooinf  39784  limccog  39852  limclner  39883  limsuppnfdlem  39933  limsupres  39937  limsupresuz2  39941  limsupequzlem  39954  limsupvaluz2  39970  supcnvlimsup  39972  limsupgtlem  40009  liminfresuz2  40019  cncfmptssg  40083  cncfuni  40099  icccncfext  40100  dvresntr  40132  dvmptresicc  40134  dvbdfbdioolem1  40143  dvdmsscn  40151  dvnxpaek  40157  dvnprodlem2  40162  stoweidlem59  40276  fourierdlem20  40344  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem52  40375  fourierdlem58  40381  fourierdlem64  40387  fourierdlem73  40396  fourierdlem76  40399  fourierdlem80  40403  fourierdlem84  40407  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  etransclem18  40469  ioorrnopnlem  40524  salincl  40543  intsal  40548  fsumlesge0  40594  sge0cl  40598  sge0supre  40606  sge0less  40609  sge0split  40626  sge0seq  40663  caragensspw  40723  omessre  40724  caragendifcl  40728  caratheodorylem1  40740  0ome  40743  omess0  40748  caragencmpl  40749  hoicvr  40762  hoissrrn  40763  hoicvrrex  40770  ovnlecvr  40772  ovnsslelem  40774  ovnssle  40775  ovnsubaddlem1  40784  hoissrrn2  40792  hoidmv1lelem1  40805  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem4  40812  ovnlecvr2  40824  voncmpl  40835  hspmbl  40843  opnvonmbllem1  40846  ovolval5lem2  40867  ovolval5lem3  40868  vonioolem1  40894  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  issmflem  40936  cnfsmf  40949  incsmflem  40950  smfsssmf  40952  smfadd  40973  decsmflem  40974  smflim  40985  smfres  40997  smfmul  41002  smfpimbor1lem1  41005  smfco  41009  smfsuplem1  41017  smfsuplem3  41019  smflimsuplem1  41026  smflimsuplem4  41029  smflimsuplem7  41032  subsubmgm  41797  elpglem1  42454