Theorem sstrid 3942

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)

Hypotheses

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

Assertion

Ref	Expression
sstrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrid

Step	Hyp	Ref	Expression
1		sstrid.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3		sstrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	sstrd 3941	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 3916

This theorem is used by:  difsymssdifssd  4210  wereu2  5648  sofld  6178  resssxp  6265  frpomin  6336  fimass  6722  fvmptss  6998  isofr2  7344  frxp  8127  fnse  8134  frxp2  8145  frxp3  8152  frrlem4  8291  frrlem13  8300  fprlem1  8302  smores2  8346  naddunif  8687  dffi3  9407  marypha1lem  9409  ordtypelem7  9502  ordtypelem8  9503  oismo  9518  unxpwdom2  9566  cantnfres  9662  oemapvali  9669  frmin  9737  frrlem15  9745  frrlem16  9746  tskwe  10012  acndom2  10114  dfac2a  10189  dfac12lem2  10204  cfle  10312  cofsmo  10328  coftr  10332  isf34lem5  10437  isf34lem7  10438  isf34lem6  10439  enfin1ai  10443  fin1a2lem12  10470  ttukeylem7  10574  alephexp1  10645  fpwwe2lem12  10708  fpwwe2  10709  canth4  10713  canthwelem  10716  pwfseqlem1  10724  pwfseqlem4  10728  fzossnn0  13805  fsuppmapnn0fiublem  14113  fsuppmapnn0fiub  14114  xptrrel  15113  limsupgle  15624  limsupgre  15628  rlimres  15705  lo1res  15706  lo1resb  15711  rlimresb  15712  o1resb  15713  o1of2  15760  o1rlimmul  15766  isercolllem2  15813  isercoll  15815  climsup  15817  fprodntriv  16089  bitsinvp1  16599  sadcaddlem  16607  sadadd2lem  16609  sadadd3  16611  sadasslem  16620  sadeq  16622  bitsres  16623  smuval2  16632  smupval  16638  smueqlem  16640  smumul  16643  1arith  17085  isstruct2  17307  setscom  17338  ressress  17405  imasvscafn  17689  imasless  17692  mrcssv  17768  isacs1i  17811  mreacs  17812  acsfn  17813  isacs4lem  18698  isacs5lem  18699  mgmhmima  18884  mhmima  19001  cntzmhm  19535  f1omvdconj  19640  f1omvdco2  19642  symgsssg  19661  symggen  19664  efgval  19911  gsumzaddlem  20115  gsumconst  20128  dmdprdd  20195  dprdfeq0  20218  dprdres  20224  dprdss  20225  dprdz  20226  subgdmdprd  20230  dprddisj2  20235  dprd2dlem1  20237  dprd2da  20238  dprd2d2  20240  dmdprdsplit2lem  20241  gsumle  20339  lmhmlsp  21304  lsppratlem4  21408  islbs3  21413  lbsextlem3  21418  znleval  21840  evpmss  21872  frlmsslsp  22082  lindff1  22106  lindfrn  22107  f1lindf  22108  lindfmm  22113  lsslindf  22116  mplcoe5  22329  mplind  22359  basdif0  23251  tgcl  23267  ppttop  23305  epttop  23307  ntrin  23359  mretopd  23390  neiptoptop  23429  cnclsi  23570  cnconst2  23581  cnrest2  23584  cnpresti  23586  cnprest2  23588  fiuncmp  23702  connsub  23719  connima  23723  iunconnlem  23725  1stcfb  23743  2ndc1stc  23749  2ndcdisj  23755  kgentopon  23837  llycmpkgen2  23849  1stckgenlem  23852  kgencn3  23857  ptclsg  23914  ptcnplem  23920  txtube  23939  hausdiag  23944  txkgen  23951  xkoco1cn  23956  xkoco2cn  23957  xkococnlem  23958  qtoptop2  23998  basqtop  24010  imastopn  24019  hmeores  24070  hmphdis  24095  ptcmpfi  24112  fbssfi  24136  filin  24153  infil  24162  fgtr  24189  elfm  24246  hausflim  24280  flimclslem  24283  fclscmp  24329  cnextcn  24366  tmdgsum2  24395  tgpconncomp  24412  ustexsym  24515  ustund  24521  ustimasn  24527  utoptop  24533  utopbas  24534  restutopopn  24537  blin2  24728  metustexhalf  24855  icccmplem2  25123  icccmplem3  25124  reconnlem2  25127  tcphcph  25538  fmcfil  25573  resscdrg  25659  ivthlem2  25753  ivthlem3  25754  ivth2  25756  ovolfiniun  25802  ovoliunlem1  25803  ismbl2  25828  nulmbl2  25837  unmbl  25838  shftmbl  25839  voliunlem1  25851  voliunlem2  25852  ioombl1lem4  25862  uniioombllem4  25887  uniioombllem5  25888  dyadmbllem  25900  dyadmbl  25901  mbflimsup  25967  i1fima  25979  i1fima2  25980  i1fadd  25996  itg1addlem4  26000  itg2splitlem  26049  itg2split  26050  ellimc3  26179  limcflflem  26180  limcflf  26181  limcresi  26185  limciun  26194  dvreslem  26209  dvres2lem  26210  dvres  26211  dvaddbr  26238  dvmulbr  26239  dvlip  26293  dvlip2  26295  c1liplem1  26296  dvivthlem1  26308  dvne0  26311  lhop1lem  26313  lhop  26316  dvcnvrelem1  26317  dvcnvrelem2  26318  dvfsumle  26321  dvfsumabs  26323  dvfsumlem2  26327  itgsubstlem  26348  mdegleb  26362  mdeglt  26363  mdegldg  26364  mdegxrcl  26365  mdegcl  26367  ig1peu  26473  reeff1olem  26755  logccv  26973  rlimcnp2  27276  lgamgulmlem2  27339  ppisval  27413  prmdvdsfi  27416  mumul  27490  sqff1o  27491  chtlepsi  27515  chpub  27529  dchrisum0lem2a  27826  pntlem3  27918  infdesc  27949  nosupno  28042  noetalem1  28080  cutlt  28300  negsproplem2  28397  onsbnd  28649  cgrabasimass  29360  ex-res  31024  htthlem  31501  chlejb1i  32060  ssmd2  32896  fz2ssnn0  33359  gsumpart  33606  gsumhashmul  33610  elrgspnsubrunlem2  33791  extvfvcl  34150  mplvrpmrhm  34161  esplyind  34189  vietalem  34193  locfinreflem  34454  sibfof  34955  sitgclbn  34958  sitgaddlemb  34963  eulerpartlemgu  34992  ballotlemsima  35131  reprinrn  35230  bnj1311  35637  fnrelpredd  35699  erdsze2lem2  35938  iccllysconn  35984  cvmopnlem  36012  msrf  36276  neiin  37090  neibastop1  37117  neibastop2lem  37118  topmeet  37122  ttciunun  37269  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem19  38525  poimirlem30  38536  cnambfre  38554  itg2gt0cn  38561  sstotbnd2  38676  sstotbnd3  38678  ssbnd  38690  ismtyima  38705  heibor1lem  38711  idresssidinxp  39214  pmodlem2  40872  pmodN  40875  diaintclN  42083  djaclN  42161  dibintclN  42192  dicval  42201  dihoml4c  42401  djhcl  42425  isnacs2  43670  isnacs3  43674  diophrw  43723  pellfundre  43841  pellfundge  43842  pellfundlb  43844  pellfundglb  43845  fnwe2lem2  44011  lmhmfgima  44044  hbt  44090  omabs2  44292  nadd2rabord  44345  nadd1rabord  44349  cnvtrcl0  44585  trclrelexplem  44670  relexp0a  44675  isotone2  45008  imo72b2lem1  45128  tcfr  45905  modelaxreplem1  45920  wfac8prim  45944  climinf  46562  islptre  46575  limccog  46576  limcleqr  46598  limsupvaluz2  46692  itgcoscmulx  46923  ismbl3  46940  ismbl4  46947  stoweidlem27  46981  dirkercncflem2  47058  fourierdlem38  47099  fourierdlem51  47111  fourierdlem54  47114  fourierdlem63  47123  fourierdlem68  47128  fourierdlem69  47129  fourierdlem70  47130  fourierdlem74  47134  fourierdlem75  47135  fourierdlem76  47136  fourierdlem80  47140  fourierdlem84  47144  fourierdlem85  47145  fourierdlem88  47148  fourierdlem100  47160  fourierdlem101  47161  fourierdlem104  47164  fourierdlem107  47167  fourierdlem111  47171  fourierdlem112  47172  caragenel2d  47486  hoidmv1lelem3  47547  hspmbllem3  47582  sssmf  47692  smfrec  47743  smfsuplem1  47765