Theorem sstrd 3944

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 3942	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 3919

This theorem is used by:  sstrid  3945  sstrdi  3946  rabssrabd  4034  ssdif2d  4098  uniintsn  4948  funss  6556  fssxp  6734  knatar  7364  tfisi  7859  suppssov1  8199  suppssov2  8200  suppssfv  8204  tposss  8229  frrlem8  8296  tfrlem1  8368  omwordri  8563  oewordri  8584  oeeui  8594  oaabs2  8641  omopthlem1  8651  ecinxp  8796  sbthlem1  9089  dffi2  9397  hartogslem1  9518  cantnfcl  9650  cantnflt  9655  cantnfp1lem3  9663  cantnflem3  9674  cnfcom  9683  cnfcom3lem  9686  ttrcltr  9699  rankssb  9834  tskwe  9959  dfac12lem2  10151  dfac12lem3  10152  cfflb  10265  cfcof  10280  ssfin2  10326  hsmexlem4  10435  ttukeylem6  10520  ttukeylem7  10521  fpwwe2lem1  10644  fpwwe2lem7  10650  fpwwe2lem10  10653  fpwwe2lem11  10654  canthnumlem  10661  canthwelem  10663  canthwe  10664  canthp1lem2  10666  pwfseqlem5  10676  wunex2  10751  tsktrss  10774  inttsk  10787  uzwo3  12996  xrsupssd  13389  supicc  13558  supiccub  13559  supicclub  13560  ssfzunsnext  13628  seqsplit  14103  seqf1olem2a  14108  seqz  14118  swrdval2  14718  swrdf1  14723  swrdrn3  14726  trrelssd  15050  rtrclreclem4  15138  sumss  15814  qshash  15918  incexc  15930  incexc2  15931  prodss  16040  rpnnen2lem11  16318  vdwlem1  17079  ramub1lem1  17124  imasaddvallem  17621  imasvscaf  17631  mrerintcl  17687  ismred2  17693  mremre  17694  mrcuni  17715  mressmrcd  17721  submrc  17722  mrissmrid  17735  mreexexlem2d  17739  isacs2  17747  isacs1i  17751  invss  17856  ssctr  17920  funcres2b  17992  isacs3lem  18636  acsfiindd  18647  acsmapd  18648  acsmap2d  18649  tsrdir  18698  subsubmgm  18818  subsubm  18931  gsumwspan  18961  subsubg  19279  subgint  19280  cntzidss  19473  symggen  19603  pmtrdifellem1  19609  pmtrdifellem2  19610  pgpssslw  19747  lsmless1x  19777  lsmless2x  19778  lsmless12  19795  subglsm  19806  gsumval3lem2  20039  gsumzaddlem  20054  gsumzadd  20055  gsum2d  20105  dmdprdd  20134  dprdfeq0  20157  dprdspan  20162  dprdres  20163  dprdss  20164  dprdz  20165  subgdmdprd  20169  subgdprd  20170  dprdsn  20171  dprd2dlem1  20176  dprd2da  20177  dmdprdsplit2lem  20180  dprdsplit  20183  pgpfac1lem2  20210  pgpfac1lem3  20212  pgpfac1lem5  20214  subsubrng  20731  subsubrg  20766  subdrgint  20975  lspss  21174  lspun  21177  lsslsp  21205  lmhmlsp  21239  lsmelval2  21275  lsmssspx  21278  lsppratlem2  21341  lsppratlem3  21342  lsppratlem4  21343  lbsextlem2  21352  lbsextlem3  21353  ssdifidllem  21553  ssdifidlprm  21555  ocvlsp  21895  cssmre  21912  obselocv  21947  obslbs  21949  aspss  22097  mhpaddcl  22385  mhpinvcl  22386  mhpvscacl  22388  psdmullem  22399  toponmre  23324  neiint  23335  neiss  23340  lpss  23373  lpss3  23375  restopnb  23406  restfpw  23410  neitr  23411  restcls  23412  restntr  23413  restlp  23414  ordtbas  23423  pnfnei  23451  mnfnei  23452  iscnp4  23494  cnclsi  23503  isreg2  23608  discmp  23629  cmpcld  23633  uncmp  23634  sscmp  23636  hauscmplem  23637  cmpfi  23639  iunconnlem  23658  clsconn  23661  2ndcctbss  23687  restnlly  23714  llyrest  23717  nllyrest  23718  llyidm  23720  nllyidm  23721  cldllycmp  23727  dislly  23729  comppfsc  23764  llycmpkgen2  23782  ptbasfi  23813  txnlly  23869  txcmplem1  23873  tx1stc  23882  xkococnlem  23891  qtopval2  23928  basqtop  23943  tgqtop  23944  qtoprest  23949  kqreglem1  23973  kqreglem2  23974  kqnrmlem1  23975  kqnrmlem2  23976  fsubbas  24099  fgabs  24111  fbasrn  24116  trfil2  24119  trfg  24123  isufil2  24140  trufil  24142  ssufl  24150  ufileu  24151  filufint  24152  fmfnfmlem4  24189  fmfnfm  24190  flimss2  24204  flimss1  24205  fclsfnflim  24259  flimfnfcls  24260  fclscmp  24262  cnpfcfi  24272  alexsubALT  24283  clssubg  24341  clsnsg  24342  tsmsres  24376  ustexsym  24448  ustex2sym  24449  ustex3sym  24450  ustneism  24456  trust  24461  utoptop  24466  restutopopn  24470  utop2nei  24482  utopreg  24484  cfiluweak  24526  neipcfilu  24527  blssps  24656  blss  24657  blcld  24737  blsscls  24739  met1stc  24753  met2ndci  24754  metust  24790  cfilucfil  24791  restmetu  24802  tgqioo  25032  xrsblre  25044  reconnlem2  25060  xrge0gsumle  25066  xrge0tsms  25067  rescncf  25131  cnmpopc  25162  cnheibor  25189  cnllycmp  25190  lebnum  25198  phtpycn  25217  cfilfcls  25508  iscmet3lem2  25526  cmetss  25550  cncmet  25556  bcthlem4  25561  bcth3  25565  rrxcph  25626  rrxmetlem  25641  minveclem4a  25664  minveclem4  25666  ivthicc  25692  ovollb  25713  ovollb2lem  25722  ovollb2  25723  nulmbl2  25770  ioorcl2  25806  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  opnmbllem  25835  volcn  25840  volivth  25841  mbfeqalem1  25875  itg10a  25944  mbfi1fseqlem4  25952  ditgcl  26092  ditgswap  26093  ditgsplitlem  26094  limcflf  26115  limcres  26120  dvbss  26135  dvbsss  26136  perfdvf  26137  dvreslem  26143  dvres2lem  26144  dvres3  26147  dvmptresicc  26150  dvcnp  26153  dvcnp2  26154  dvcn  26155  dvnff  26157  dvn2bss  26164  dvnres  26165  cpnord  26169  dvaddbr  26172  dvmulbr  26173  dvcobr  26180  dvnfre  26186  dvmptres2  26196  dvmptntr  26205  dvcnvlem  26210  dvcnv  26211  dvferm1lem  26218  dvferm2lem  26220  dvlip  26227  dvlipcn  26228  dvlip2  26229  c1liplem1  26230  dvgt0lem1  26236  lhop1lem  26247  lhop  26250  dvcnvrelem1  26251  dvcnvrelem2  26252  dvcnvre  26253  dvfsumle  26255  dvfsumge  26256  dvfsumabs  26257  ftc1lem1  26269  ftc1lem2  26270  ftc1a  26271  ftc1lem4  26273  ftc2ditglem  26279  itgsubstlem  26282  ig1peu  26407  ig1pdvds  26412  taylfvallem1  26600  tayl0  26605  taylply2  26611  taylply  26612  dvtaylp  26613  dvntaylp  26614  dvntaylp0  26615  taylthlem1  26616  ulmdvlem1  26643  ulmdvlem3  26645  psercn  26669  pserdvlem2  26671  abelth  26684  xrlimcnp  27213  lgamucov  27282  wilthlem2  27313  sqff1o  27426  chtublem  27455  pntlemq  27845  pntlemf  27849  ssslts1  28046  ssslts2  28047  cutbdaybnd  28068  cutbdaybnd2  28069  eqcuts3  28077  cofss  28203  coiniss  28204  bdaypw2bnd  28738  bdayfinbndlem1  28740  z12bdaylem2  28744  tglineintmo  28997  ttgcontlem1  29349  pthdlem1  30239  shintcli  31818  shub1  31871  mdslmd1lem1  32814  mdexchi  32824  chirredlem1  32879  mdsymlem5  32896  sumdmdii  32904  sumdmdlem2  32908  fnpreimac  33151  fsuppinisegfi  33167  xrge0infssd  33240  swrdrndisj  33405  pwrssmgc  33448  xrge0tsmsd  33521  elrgspnlem4  33693  elrgspnsubrunlem1  33695  elrgspnsubrunlem2  33696  fldgenss  33765  fldgenssp  33767  linds2eq  33822  elrspunidl  33864  mxidlprm  33881  ssmxidllem  33884  ssmxidl  33885  qsdrnglem2  33906  rprmdvdsprod  33952  ressply1evls1  33983  resssra  34105  lsssra  34106  exsslsb  34115  lbsdiflsp0  34144  dimkerim  34145  fedgmullem1  34147  fedgmullem2  34148  fedgmul  34149  dimlssid  34150  fldextrspunlsplem  34191  fldextrspunlsp  34192  fldextrspunlem1  34193  fldextrspundgdvdslem  34198  fldextrspundgdvds  34199  constr01  34260  constrmon  34262  constrextdg2lem  34266  constrfiss  34269  smatrcl  34314  locfinreflem  34358  cmpcref  34368  zarclsun  34388  zarclsiin  34389  zarclssn  34391  zarcmplem  34399  pnfneige0  34469  esum2d  34611  insiga  34656  sssigagen2  34665  dynkin  34686  dya2iocnei  34801  omsmon  34817  carsgclctunlem1  34836  carsggect  34837  omsmeas  34842  ftc2re  35114  fdvneggt  35116  fdvnegge  35118  reprsuc  35131  reprss  35133  reprlt  35135  reprinfz1  35138  logdivsqrle  35166  hgt750lemb  35172  bnj906  35447  bnj1020  35482  bnj1137  35512  bnj1408  35553  bnj1452  35569  rankval4b  35615  fineqvnttrclselem2  35656  erdszelem7  35784  erdszelem8  35785  erdsze2lem1  35790  connpconn  35822  cvmliftmolem1  35868  cvmlift2lem1  35889  cvmlift2lem9  35898  cvmlift2lem10  35899  cvmlift3lem6  35911  cvmlift3lem7  35912  satfsschain  35951  ss2mcls  36155  neibastop2lem  36987  fnemeet2  36994  fnejoin1  36995  ontgval  37058  ttcmin  37123  unbdqndv1  37213  opnmbllem0  38413  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  sstotbnd2  38532  heiborlem1  38569  heiborlem8  38576  intidl  38787  lsmsat  39889  lssats  39893  lpssat  39894  lssatle  39896  lssat  39897  lsatcvatlem  39930  paddss12  40700  paddasslem17  40717  pmodlem1  40727  pmod1i  40729  pmodl42N  40732  elpcliN  40774  pclfinN  40781  polcon3N  40798  polcon2N  40800  paddunN  40808  pclfinclN  40831  poml5N  40835  osumcllem1N  40837  osumcllem2N  40838  osumcllem3N  40839  pl42lem2N  40861  pl42lem4N  40863  cdlemn5pre  42081  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord5b  42140  dochss  42246  dochdmj1  42271  djhsumss  42288  djhunssN  42290  dochexmidlem2  42342  lclkrslem1  42418  lclkrslem2  42419  lcfrlem2  42424  aks4d1p4  42953  aks4d1p5  42954  aks4d1p7  42957  aks4d1p8  42961  aks6d1c2  43004  sticksstones1  43020  unitscyglem5  43073  prjcrv0  43487  elrfi  43547  ismrcd1  43551  istopclsd  43553  mrefg2  43560  aomclem2  43904  aomclem6  43908  hbtlem6  43978  hbt  43979  oege2  44156  cantnftermord  44169  omabs2  44181  tfsconcat0b  44195  naddgeoa  44243  naddwordnexlem0  44245  naddwordnexlem1  44246  dfno2  44276  mptrcllem  44461  dfrcl2  44522  relexp0a  44564  trclimalb2  44574  frege81d  44595  k0004ss2  45000  imo72b2lem2  45015  imo72b2  45020  uzwo4  45895  ssin0  45897  ixpssmapc  45915  ssinc  45927  ssdec  45928  supxrre3  46163  uzfissfz  46164  ssuzfz  46187  supminfxr  46300  inficc  46372  ressiocsup  46392  ressioosup  46393  ressiooinf  46395  limccog  46458  limclner  46487  limsupres  46541  limsupresuz2  46545  limsupequzlem  46558  supcnvlimsup  46576  limsupgtlem  46613  liminfresuz2  46623  cncfmptssg  46707  icccncfext  46723  dvresntr  46754  dvbdfbdioolem1  46764  dvdmsscn  46772  dvnxpaek  46778  dvnprodlem2  46783  stoweidlem59  46895  fourierdlem20  46963  fourierdlem42  46985  fourierdlem48  46990  fourierdlem49  46991  fourierdlem52  46994  fourierdlem58  47000  fourierdlem64  47006  fourierdlem73  47015  fourierdlem76  47018  fourierdlem80  47022  fourierdlem84  47026  fourierdlem93  47035  fourierdlem103  47045  fourierdlem104  47046  fourierdlem113  47055  etransclem18  47088  ioorrnopnlem  47140  salincl  47160  intsal  47166  fsumlesge0  47213  sge0cl  47217  sge0supre  47225  sge0less  47228  sge0split  47245  sge0seq  47282  caragensspw  47345  omessre  47346  caragendifcl  47350  caratheodorylem1  47362  0ome  47365  omess0  47370  caragencmpl  47371  hoissrrn  47385  hoicvrrex  47392  ovnlecvr  47394  ovnsslelem  47396  ovnssle  47397  ovnsubaddlem1  47406  hoissrrn2  47414  hoidmv1lelem1  47427  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem4  47434  ovnlecvr2  47446  voncmpl  47457  hspmbl  47465  opnvonmbllem1  47468  ovolval5lem2  47489  ovolval5lem3  47490  vonioolem1  47516  pimdecfgtioc  47551  pimincfltioc  47552  pimdecfgtioo  47553  pimincfltioo  47554  issmflem  47563  cnfsmf  47576  incsmflem  47577  smfsssmf  47579  smfadd  47601  decsmflem  47602  smflim  47613  smfres  47626  smfmul  47631  smfpimbor1lem1  47634  smfco  47638  smfsuplem1  47647  smfsuplem3  47649  smflimsuplem1  47656  smflimsuplem4  47659  smflimsuplem7  47662  tmachlem-agreeprod  47773  nndivides2  48280  cnneiima  49851  seposep  49860  iscnrm3rlem4  49877  iscnrm3llem1  49883  lubsscl  49894  glbsscl  49895  toplatglb  49935  setrecsss  50635  elpglem1  50645