Theorem sstrid 3947

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 3946	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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

This proof depends on definitions:  df-bi 210  df-an 401  df-ss 3921

This theorem is used by:  difsymssdifssd  4216  wereu2  5657  sofld  6184  resssxp  6271  frpomin  6341  fimass  6726  fvmptss  7002  isofr2  7342  frxp  8120  fnse  8127  frxp2  8138  frxp3  8145  frrlem4  8284  frrlem13  8293  fprlem1  8295  smores2  8339  naddunif  8678  dffi3  9389  marypha1lem  9391  ordtypelem7  9484  ordtypelem8  9485  oismo  9500  unxpwdom2  9548  cantnfres  9644  oemapvali  9651  frmin  9719  frrlem15  9727  frrlem16  9728  tskwe  9943  acndom2  10045  dfac2a  10120  dfac12lem2  10135  cfle  10243  cofsmo  10259  coftr  10263  isf34lem5  10368  isf34lem7  10369  isf34lem6  10370  enfin1ai  10374  fin1a2lem12  10401  ttukeylem7  10505  alephexp1  10570  fpwwe2lem12  10633  fpwwe2  10634  canth4  10638  canthwelem  10641  pwfseqlem1  10649  pwfseqlem4  10653  fzossnn0  13726  fsuppmapnn0fiublem  14033  fsuppmapnn0fiub  14034  xptrrel  15024  limsupgle  15535  limsupgre  15539  rlimres  15616  lo1res  15617  lo1resb  15622  rlimresb  15623  o1resb  15624  o1of2  15671  o1rlimmul  15677  isercolllem2  15724  isercoll  15726  climsup  15728  fprodntriv  16003  bitsinvp1  16513  sadcaddlem  16521  sadadd2lem  16523  sadadd3  16525  sadasslem  16534  sadeq  16536  bitsres  16537  smuval2  16546  smupval  16552  smueqlem  16554  smumul  16557  1arith  16993  isstruct2  17215  setscom  17246  ressress  17313  imasvscafn  17597  imasless  17600  mrcssv  17676  isacs1i  17719  mreacs  17720  acsfn  17721  isacs4lem  18606  isacs5lem  18607  mgmhmima  18779  mhmima  18890  cntzmhm  19417  f1omvdconj  19522  f1omvdco2  19524  symgsssg  19543  symggen  19546  efgval  19793  gsumzaddlem  19997  gsumconst  20010  dmdprdd  20077  dprdfeq0  20100  dprdres  20106  dprdss  20107  dprdz  20108  subgdmdprd  20112  dprddisj2  20117  dprd2dlem1  20119  dprd2da  20120  dprd2d2  20122  dmdprdsplit2lem  20123  gsumle  20221  lmhmlsp  21181  lsppratlem4  21285  islbs3  21290  lbsextlem3  21295  znleval  21715  evpmss  21747  frlmsslsp  21957  lindff1  21981  lindfrn  21982  f1lindf  21983  lindfmm  21988  lsslindf  21991  mplcoe5  22202  mplind  22232  basdif0  23121  tgcl  23137  ppttop  23175  epttop  23177  ntrin  23229  mretopd  23260  neiptoptop  23299  cnclsi  23440  cnconst2  23451  cnrest2  23454  cnpresti  23456  cnprest2  23458  fiuncmp  23572  connsub  23589  connima  23593  iunconnlem  23595  1stcfb  23613  2ndc1stc  23619  2ndcdisj  23624  kgentopon  23706  llycmpkgen2  23718  1stckgenlem  23721  kgencn3  23726  ptclsg  23783  ptcnplem  23789  txtube  23808  hausdiag  23813  txkgen  23820  xkoco1cn  23825  xkoco2cn  23826  xkococnlem  23827  qtoptop2  23867  basqtop  23879  imastopn  23888  hmeores  23939  hmphdis  23964  ptcmpfi  23981  fbssfi  24005  filin  24022  infil  24031  fgtr  24058  elfm  24115  hausflim  24149  flimclslem  24152  fclscmp  24198  cnextcn  24235  tmdgsum2  24264  tgpconncomp  24281  ustexsym  24384  ustund  24390  ustimasn  24396  utoptop  24402  utopbas  24403  restutopopn  24406  blin2  24597  metustexhalf  24724  icccmplem2  24992  icccmplem3  24993  reconnlem2  24996  tcphcph  25407  fmcfil  25442  resscdrg  25528  ivthlem2  25622  ivthlem3  25623  ivth2  25625  ovolfiniun  25671  ovoliunlem1  25672  ismbl2  25697  nulmbl2  25706  unmbl  25707  shftmbl  25708  voliunlem1  25720  voliunlem2  25721  ioombl1lem4  25731  uniioombllem4  25756  uniioombllem5  25757  dyadmbllem  25769  dyadmbl  25770  mbflimsup  25836  i1fima  25848  i1fima2  25849  i1fadd  25865  itg1addlem4  25869  itg2splitlem  25918  itg2split  25919  ellimc3  26049  limcflflem  26050  limcflf  26051  limcresi  26055  limciun  26064  dvreslem  26079  dvres2lem  26080  dvres  26081  dvaddbr  26108  dvmulbr  26109  dvlip  26163  dvlip2  26165  c1liplem1  26166  dvivthlem1  26178  dvne0  26181  lhop1lem  26183  lhop  26186  dvcnvrelem1  26187  dvcnvrelem2  26188  dvfsumle  26191  dvfsumabs  26193  dvfsumlem2  26197  itgsubstlem  26218  mdegleb  26232  mdeglt  26233  mdegldg  26234  mdegxrcl  26235  mdegcl  26237  ig1peu  26343  reeff1olem  26620  logccv  26839  rlimcnp2  27142  lgamgulmlem2  27205  ppisval  27279  prmdvdsfi  27282  mumul  27356  sqff1o  27357  chtlepsi  27381  chpub  27395  dchrisum0lem2a  27692  pntlem3  27784  nosupno  27878  noetalem1  27916  cutlt  28136  negsproplem2  28233  onsbnd  28485  ex-res  30803  htthlem  31280  chlejb1i  31839  ssmd2  32675  fz2ssnn0  33141  gsumpart  33392  gsumhashmul  33396  elrgspnsubrunlem2  33577  extvfvcl  33935  mplvrpmrhm  33946  esplyind  33974  vietalem  33978  locfinreflem  34239  sibfof  34739  sitgclbn  34742  sitgaddlemb  34747  eulerpartlemgu  34776  ballotlemsima  34915  reprinrn  35014  bnj1311  35421  fnrelpredd  35491  erdsze2lem2  35704  iccllysconn  35750  cvmopnlem  35778  msrf  36042  neiin  36871  neibastop1  36898  neibastop2lem  36899  topmeet  36903  ttciunun  37050  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem11  38310  poimirlem12  38311  poimirlem16  38315  poimirlem19  38318  poimirlem30  38329  cnambfre  38347  itg2gt0cn  38354  sstotbnd2  38453  sstotbnd3  38455  ssbnd  38467  ismtyima  38482  heibor1lem  38488  idresssidinxp  38991  pmodlem2  40649  pmodN  40652  diaintclN  41860  djaclN  41938  dibintclN  41969  dicval  41978  dihoml4c  42178  djhcl  42202  infdesc  43403  isnacs2  43465  isnacs3  43469  diophrw  43518  pellfundre  43636  pellfundge  43637  pellfundlb  43639  pellfundglb  43640  fnwe2lem2  43806  lmhmfgima  43839  hbt  43885  omabs2  44087  nadd2rabord  44140  nadd1rabord  44144  cnvtrcl0  44380  trclrelexplem  44465  relexp0a  44470  isotone2  44803  imo72b2lem1  44923  tcfr  45700  modelaxreplem1  45715  wfac8prim  45739  climinf  46350  islptre  46363  limccog  46364  limcleqr  46386  limsupvaluz2  46480  itgcoscmulx  46711  ismbl3  46728  ismbl4  46735  stoweidlem27  46769  dirkercncflem2  46846  fourierdlem38  46887  fourierdlem51  46899  fourierdlem54  46902  fourierdlem63  46911  fourierdlem68  46916  fourierdlem69  46917  fourierdlem70  46918  fourierdlem74  46922  fourierdlem75  46923  fourierdlem76  46924  fourierdlem80  46928  fourierdlem84  46932  fourierdlem85  46933  fourierdlem88  46936  fourierdlem100  46948  fourierdlem101  46949  fourierdlem104  46952  fourierdlem107  46955  fourierdlem111  46959  fourierdlem112  46960  caragenel2d  47274  hoidmv1lelem3  47335  hspmbllem3  47370  sssmf  47480  smfrec  47531  smfsuplem1  47553