Theorem sstrd 3950

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

Hypotheses

Ref	Expression
sstrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sstrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
sstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		sstr 3948	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3925

This theorem is used by:  sstrid  3951  sstrdi  3952  rabssrabd  4040  ssdif2d  4105  uniintsn  4955  funss  6562  fssxp  6740  knatar  7368  tfisi  7864  suppssov1  8202  suppssov2  8203  suppssfv  8207  tposss  8232  frrlem8  8299  tfrlem1  8371  omwordri  8566  oewordri  8587  oeeui  8597  oaabs2  8644  omopthlem1  8654  ecinxp  8799  sbthlem1  9085  dffi2  9393  hartogslem1  9514  cantnfcl  9646  cantnflt  9651  cantnfp1lem3  9659  cantnflem3  9670  cnfcom  9679  cnfcom3lem  9682  ttrcltr  9695  rankssb  9830  tskwe  9955  dfac12lem2  10147  dfac12lem3  10148  cfflb  10261  cfcof  10276  ssfin2  10322  hsmexlem4  10431  ttukeylem6  10516  ttukeylem7  10517  fpwwe2lem1  10634  fpwwe2lem7  10640  fpwwe2lem10  10643  fpwwe2lem11  10644  canthnumlem  10651  canthwelem  10653  canthwe  10654  canthp1lem2  10656  pwfseqlem5  10666  wunex2  10741  tsktrss  10764  inttsk  10777  uzwo3  12985  xrsupssd  13377  supicc  13546  supiccub  13547  supicclub  13548  ssfzunsnext  13616  seqsplit  14091  seqf1olem2a  14096  seqz  14106  swrdval2  14706  swrdf1  14711  swrdrn3  14714  trrelssd  15036  rtrclreclem4  15124  sumss  15801  qshash  15905  incexc  15917  incexc2  15918  prodss  16027  rpnnen2lem11  16305  vdwlem1  17066  ramub1lem1  17111  imasaddvallem  17608  imasvscaf  17618  mrerintcl  17674  ismred2  17680  mremre  17681  mrcuni  17702  mressmrcd  17708  submrc  17709  mrissmrid  17722  mreexexlem2d  17726  isacs2  17734  isacs1i  17738  invss  17843  ssctr  17907  funcres2b  17979  isacs3lem  18623  acsfiindd  18634  acsmapd  18635  acsmap2d  18636  tsrdir  18685  subsubmgm  18797  subsubm  18906  gsumwspan  18936  subsubg  19247  subgint  19248  cntzidss  19441  symggen  19571  pmtrdifellem1  19577  pmtrdifellem2  19578  pgpssslw  19715  lsmless1x  19745  lsmless2x  19746  lsmless12  19763  subglsm  19774  gsumval3lem2  20007  gsumzaddlem  20022  gsumzadd  20023  gsum2d  20073  dmdprdd  20102  dprdfeq0  20125  dprdspan  20130  dprdres  20131  dprdss  20132  dprdz  20133  subgdmdprd  20137  subgdprd  20138  dprdsn  20139  dprd2dlem1  20144  dprd2da  20145  dmdprdsplit2lem  20148  dprdsplit  20151  pgpfac1lem2  20178  pgpfac1lem3  20180  pgpfac1lem5  20182  subsubrng  20699  subsubrg  20734  subdrgint  20943  lspss  21142  lspun  21145  lsslsp  21173  lmhmlsp  21207  lsmelval2  21243  lsmssspx  21246  lsppratlem2  21309  lsppratlem3  21310  lsppratlem4  21311  lbsextlem2  21320  lbsextlem3  21321  ssdifidllem  21521  ssdifidlprm  21523  ocvlsp  21863  cssmre  21880  obselocv  21915  obslbs  21917  aspss  22063  mhpaddcl  22351  mhpinvcl  22352  mhpvscacl  22354  psdmullem  22365  toponmre  23287  neiint  23298  neiss  23303  lpss  23336  lpss3  23338  restopnb  23369  restfpw  23373  neitr  23374  restcls  23375  restntr  23376  restlp  23377  ordtbas  23386  pnfnei  23414  mnfnei  23415  iscnp4  23457  cnclsi  23466  isreg2  23571  discmp  23592  cmpcld  23596  uncmp  23597  sscmp  23599  hauscmplem  23600  cmpfi  23602  iunconnlem  23621  clsconn  23624  2ndcctbss  23649  restnlly  23676  llyrest  23679  nllyrest  23680  llyidm  23682  nllyidm  23683  cldllycmp  23689  dislly  23691  comppfsc  23726  llycmpkgen2  23744  ptbasfi  23775  txnlly  23831  txcmplem1  23835  tx1stc  23844  xkococnlem  23853  qtopval2  23890  basqtop  23905  tgqtop  23906  qtoprest  23911  kqreglem1  23935  kqreglem2  23936  kqnrmlem1  23937  kqnrmlem2  23938  fsubbas  24061  fgabs  24073  fbasrn  24078  trfil2  24081  trfg  24085  isufil2  24102  trufil  24104  ssufl  24112  ufileu  24113  filufint  24114  fmfnfmlem4  24151  fmfnfm  24152  flimss2  24166  flimss1  24167  fclsfnflim  24221  flimfnfcls  24222  fclscmp  24224  cnpfcfi  24234  alexsubALT  24245  clssubg  24303  clsnsg  24304  tsmsres  24338  ustexsym  24410  ustex2sym  24411  ustex3sym  24412  ustneism  24418  trust  24423  utoptop  24428  restutopopn  24432  utop2nei  24444  utopreg  24446  cfiluweak  24488  neipcfilu  24489  blssps  24618  blss  24619  blcld  24699  blsscls  24701  met1stc  24715  met2ndci  24716  metust  24752  cfilucfil  24753  restmetu  24764  tgqioo  24994  xrsblre  25006  reconnlem2  25022  xrge0gsumle  25028  xrge0tsms  25029  rescncf  25093  cnmpopc  25124  cnheibor  25151  cnllycmp  25152  lebnum  25160  phtpycn  25179  cfilfcls  25470  iscmet3lem2  25488  cmetss  25512  cncmet  25518  bcthlem4  25523  bcth3  25527  rrxcph  25588  rrxmetlem  25603  minveclem4a  25626  minveclem4  25628  ivthicc  25654  ovollb  25675  ovollb2lem  25684  ovollb2  25685  nulmbl2  25732  ioorcl2  25768  uniioombllem3  25781  uniioombllem4  25782  uniioombllem5  25783  opnmbllem  25797  volcn  25802  volivth  25803  mbfeqalem1  25837  itg10a  25906  mbfi1fseqlem4  25914  ditgcl  26054  ditgswap  26055  ditgsplitlem  26056  limcflf  26077  limcres  26082  dvbss  26097  dvbsss  26098  perfdvf  26099  dvreslem  26105  dvres2lem  26106  dvres3  26109  dvmptresicc  26112  dvcnp  26115  dvcnp2  26116  dvcn  26117  dvnff  26119  dvn2bss  26126  dvnres  26127  cpnord  26131  dvaddbr  26134  dvmulbr  26135  dvcobr  26142  dvnfre  26148  dvmptres2  26158  dvmptntr  26167  dvcnvlem  26172  dvcnv  26173  dvferm1lem  26180  dvferm2lem  26182  dvlip  26189  dvlipcn  26190  dvlip2  26191  c1liplem1  26192  dvgt0lem1  26198  lhop1lem  26209  lhop  26212  dvcnvrelem1  26213  dvcnvrelem2  26214  dvcnvre  26215  dvfsumle  26217  dvfsumge  26218  dvfsumabs  26219  ftc1lem1  26231  ftc1lem2  26232  ftc1a  26233  ftc1lem4  26235  ftc2ditglem  26241  itgsubstlem  26244  ig1peu  26369  ig1pdvds  26374  taylfvallem1  26557  tayl0  26562  taylply2  26568  taylply  26569  dvtaylp  26570  dvntaylp  26571  dvntaylp0  26572  taylthlem1  26573  ulmdvlem1  26600  ulmdvlem3  26602  psercn  26626  pserdvlem2  26628  abelth  26641  xrlimcnp  27170  lgamucov  27239  wilthlem2  27270  sqff1o  27383  chtublem  27412  pntlemq  27802  pntlemf  27806  ssslts1  28003  ssslts2  28004  cutbdaybnd  28025  cutbdaybnd2  28026  eqcuts3  28034  cofss  28160  coiniss  28161  bdaypw2bnd  28695  bdayfinbndlem1  28697  z12bdaylem2  28701  tglineintmo  28952  ttgcontlem1  29271  pthdlem1  30152  shintcli  31718  shub1  31771  mdslmd1lem1  32714  mdexchi  32724  chirredlem1  32779  mdsymlem5  32796  sumdmdii  32804  sumdmdlem2  32808  fnpreimac  33052  fsuppinisegfi  33069  xrge0infssd  33143  swrdrndisj  33308  pwrssmgc  33351  xrge0tsmsd  33424  elrgspnlem4  33596  elrgspnsubrunlem1  33598  elrgspnsubrunlem2  33599  fldgenss  33668  fldgenssp  33670  linds2eq  33725  elrspunidl  33767  mxidlprm  33784  ssmxidllem  33787  ssmxidl  33788  qsdrnglem2  33809  rprmdvdsprod  33855  ressply1evls1  33886  resssra  34008  lsssra  34009  exsslsb  34018  lbsdiflsp0  34047  dimkerim  34048  fedgmullem1  34050  fedgmullem2  34051  fedgmul  34052  dimlssid  34053  fldextrspunlsplem  34094  fldextrspunlsp  34095  fldextrspunlem1  34096  fldextrspundgdvdslem  34101  fldextrspundgdvds  34102  constr01  34163  constrmon  34165  constrextdg2lem  34169  constrfiss  34172  smatrcl  34217  locfinreflem  34261  cmpcref  34271  zarclsun  34291  zarclsiin  34292  zarclssn  34294  zarcmplem  34302  pnfneige0  34372  esum2d  34514  insiga  34558  sssigagen2  34567  dynkin  34588  dya2iocnei  34703  omsmon  34719  carsgclctunlem1  34738  carsggect  34739  omsmeas  34744  ftc2re  35016  fdvneggt  35018  fdvnegge  35020  reprsuc  35033  reprss  35035  reprlt  35037  reprinfz1  35040  logdivsqrle  35068  hgt750lemb  35074  bnj906  35349  bnj1020  35384  bnj1137  35414  bnj1408  35455  bnj1452  35471  rankval4b  35517  fineqvnttrclselem2  35558  erdszelem7  35709  erdszelem8  35710  erdsze2lem1  35715  connpconn  35747  cvmliftmolem1  35793  cvmlift2lem1  35814  cvmlift2lem9  35823  cvmlift2lem10  35824  cvmlift3lem6  35836  cvmlift3lem7  35837  satfsschain  35876  ss2mcls  36080  neibastop2lem  36911  fnemeet2  36918  fnejoin1  36919  ontgval  36982  ttcmin  37047  unbdqndv1  37137  opnmbllem0  38347  ftc1anclem7  38390  ftc1anclem8  38391  ftc1anc  38392  sstotbnd2  38465  heiborlem1  38502  heiborlem8  38509  intidl  38720  lsmsat  39822  lssats  39826  lpssat  39827  lssatle  39829  lssat  39830  lsatcvatlem  39863  paddss12  40633  paddasslem17  40650  pmodlem1  40660  pmod1i  40662  pmodl42N  40665  elpcliN  40707  pclfinN  40714  polcon3N  40731  polcon2N  40733  paddunN  40741  pclfinclN  40764  poml5N  40768  osumcllem1N  40770  osumcllem2N  40771  osumcllem3N  40772  pl42lem2N  40794  pl42lem4N  40796  cdlemn5pre  42014  dihord1  42032  dihord2a  42033  dihord2b  42034  dihord5b  42073  dochss  42179  dochdmj1  42204  djhsumss  42221  djhunssN  42223  dochexmidlem2  42275  lclkrslem1  42351  lclkrslem2  42352  lcfrlem2  42357  aks4d1p4  42886  aks4d1p5  42887  aks4d1p7  42890  aks4d1p8  42894  aks6d1c2  42937  sticksstones1  42953  unitscyglem5  43006  prjcrv0  43405  elrfi  43465  ismrcd1  43469  istopclsd  43471  mrefg2  43478  aomclem2  43822  aomclem6  43826  hbtlem6  43896  hbt  43897  oege2  44074  cantnftermord  44087  omabs2  44099  tfsconcat0b  44113  naddgeoa  44161  naddwordnexlem0  44163  naddwordnexlem1  44164  dfno2  44194  mptrcllem  44379  dfrcl2  44440  relexp0a  44482  trclimalb2  44492  frege81d  44513  k0004ss2  44918  imo72b2lem2  44933  imo72b2  44938  uzwo4  45813  ssin0  45815  ixpssmapc  45833  ssinc  45845  ssdec  45846  supxrre3  46081  uzfissfz  46082  ssuzfz  46105  supminfxr  46218  inficc  46290  ressiocsup  46310  ressioosup  46311  ressiooinf  46313  limccog  46376  limclner  46405  limsupres  46459  limsupresuz2  46463  limsupequzlem  46476  supcnvlimsup  46494  limsupgtlem  46531  liminfresuz2  46541  cncfmptssg  46625  icccncfext  46641  dvresntr  46672  dvbdfbdioolem1  46682  dvdmsscn  46690  dvnxpaek  46696  dvnprodlem2  46701  stoweidlem59  46813  fourierdlem20  46881  fourierdlem42  46903  fourierdlem48  46908  fourierdlem49  46909  fourierdlem52  46912  fourierdlem58  46918  fourierdlem64  46924  fourierdlem73  46933  fourierdlem76  46936  fourierdlem80  46940  fourierdlem84  46944  fourierdlem93  46953  fourierdlem103  46963  fourierdlem104  46964  fourierdlem113  46973  etransclem18  47006  ioorrnopnlem  47058  salincl  47078  intsal  47084  fsumlesge0  47131  sge0cl  47135  sge0supre  47143  sge0less  47146  sge0split  47163  sge0seq  47200  caragensspw  47263  omessre  47264  caragendifcl  47268  caratheodorylem1  47280  0ome  47283  omess0  47288  caragencmpl  47289  hoissrrn  47303  hoicvrrex  47310  ovnlecvr  47312  ovnsslelem  47314  ovnssle  47315  ovnsubaddlem1  47324  hoissrrn2  47332  hoidmv1lelem1  47345  hoidmvlelem1  47349  hoidmvlelem2  47350  hoidmvlelem4  47352  ovnlecvr2  47364  voncmpl  47375  hspmbl  47383  opnvonmbllem1  47386  ovolval5lem2  47407  ovolval5lem3  47408  vonioolem1  47434  pimdecfgtioc  47469  pimincfltioc  47470  pimdecfgtioo  47471  pimincfltioo  47472  issmflem  47481  cnfsmf  47494  incsmflem  47495  smfsssmf  47497  smfadd  47519  decsmflem  47520  smflim  47531  smfres  47544  smfmul  47549  smfpimbor1lem1  47552  smfco  47556  smfsuplem1  47565  smfsuplem3  47567  smflimsuplem1  47574  smflimsuplem4  47577  smflimsuplem7  47580  nndivides2  48161  cnneiima  49735  seposep  49744  iscnrm3rlem4  49761  iscnrm3llem1  49767  lubsscl  49778  glbsscl  49779  toplatglb  49819  setrecsss  50519  elpglem1  50529