Theorem sstrid 3926

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

Syntax hints:   → wi 4   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  difsymssdifssd  4180  wereu2  5516  sofld  6011  resssxp  6089  fimass  6529  fvmptss  6757  fimacnv  6816  isofr2  7076  frxp  7803  fnse  7810  smores2  7974  dffi3  8879  marypha1lem  8881  ordtypelem7  8972  ordtypelem8  8973  oismo  8988  unxpwdom2  9036  cantnfres  9124  oemapvali  9131  tskwe  9363  acndom2  9465  dfac2a  9540  dfac12lem2  9555  cfle  9665  cofsmo  9680  coftr  9684  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  enfin1ai  9795  fin1a2lem12  9822  ttukeylem7  9926  alephexp1  9990  fpwwe2lem13  10053  fpwwe2  10054  canth4  10058  canthwelem  10061  pwfseqlem1  10069  pwfseqlem4  10073  fzossnn0  13063  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  xptrrel  14331  limsupgle  14826  limsupgre  14830  rlimres  14907  lo1res  14908  lo1resb  14913  rlimresb  14914  o1resb  14915  o1of2  14961  o1rlimmul  14967  isercolllem2  15014  isercoll  15016  climsup  15018  fprodntriv  15288  bitsinvp1  15788  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadasslem  15809  sadeq  15811  bitsres  15812  smuval2  15821  smupval  15827  smueqlem  15829  smumul  15832  1arith  16253  isstruct2  16485  setscom  16519  ressress  16554  imasvscafn  16802  imasless  16805  mrcssv  16877  isacs1i  16920  mreacs  16921  acsfn  16922  isacs4lem  17770  isacs5lem  17771  mhmima  17981  cntzmhm  18461  f1omvdconj  18566  f1omvdco2  18568  symgsssg  18587  symggen  18590  efgval  18835  gsumzaddlem  19034  gsumconst  19047  dmdprdd  19114  dprdfeq0  19137  dprdres  19143  dprdss  19144  dprdz  19145  subgdmdprd  19149  dprddisj2  19154  dprd2dlem1  19156  dprd2da  19157  dprd2d2  19159  dmdprdsplit2lem  19160  lmhmlsp  19814  lsppratlem4  19915  islbs3  19920  lbsextlem3  19925  znleval  20246  evpmss  20275  frlmsslsp  20485  lindff1  20509  lindfrn  20510  f1lindf  20511  lindfmm  20516  lsslindf  20519  mplcoe5  20708  mplind  20741  basdif0  21558  tgcl  21574  ppttop  21612  epttop  21614  ntrin  21666  mretopd  21697  neiptoptop  21736  cnclsi  21877  cnconst2  21888  cnrest2  21891  cnpresti  21893  cnprest2  21895  fiuncmp  22009  connsub  22026  connima  22030  iunconnlem  22032  1stcfb  22050  2ndc1stc  22056  2ndcdisj  22061  kgentopon  22143  llycmpkgen2  22155  1stckgenlem  22158  kgencn3  22163  ptclsg  22220  ptcnplem  22226  txtube  22245  hausdiag  22250  txkgen  22257  xkoco1cn  22262  xkoco2cn  22263  xkococnlem  22264  qtoptop2  22304  basqtop  22316  imastopn  22325  hmeores  22376  hmphdis  22401  ptcmpfi  22418  fbssfi  22442  filin  22459  infil  22468  fgtr  22495  elfm  22552  hausflim  22586  flimclslem  22589  fclscmp  22635  cnextcn  22672  tmdgsum2  22701  tgpconncomp  22718  ustexsym  22821  ustund  22827  ustimasn  22834  utoptop  22840  utopbas  22841  restutopopn  22844  blin2  23036  metustexhalf  23163  icccmplem2  23428  icccmplem3  23429  reconnlem2  23432  tcphcph  23841  fmcfil  23876  resscdrg  23962  ivthlem2  24056  ivthlem3  24057  ivth2  24059  ovolfiniun  24105  ovoliunlem1  24106  ismbl2  24131  nulmbl2  24140  unmbl  24141  shftmbl  24142  voliunlem1  24154  voliunlem2  24155  ioombl1lem4  24165  uniioombllem4  24190  uniioombllem5  24191  dyadmbllem  24203  dyadmbl  24204  mbflimsup  24270  i1fima  24282  i1fima2  24283  i1fadd  24299  itg1addlem4  24303  itg2splitlem  24352  itg2split  24353  ellimc3  24482  limcflflem  24483  limcflf  24484  limcresi  24488  limciun  24497  dvreslem  24512  dvres2lem  24513  dvres  24514  dvaddbr  24541  dvmulbr  24542  dvlip  24596  dvlip2  24598  c1liplem1  24599  dvivthlem1  24611  dvne0  24614  lhop1lem  24616  lhop  24619  dvcnvrelem1  24620  dvcnvrelem2  24621  dvfsumle  24624  dvfsumabs  24626  dvfsumlem2  24630  itgsubstlem  24651  mdegleb  24665  mdeglt  24666  mdegldg  24667  mdegxrcl  24668  mdegcl  24670  ig1peu  24772  reeff1olem  25041  logccv  25254  rlimcnp2  25552  lgamgulmlem2  25615  ppisval  25689  prmdvdsfi  25692  mumul  25766  sqff1o  25767  chtlepsi  25790  chpub  25804  dchrisum0lem2a  26101  pntlem3  26193  ex-res  28226  htthlem  28700  chlejb1i  29259  ssmd2  30095  fz2ssnn0  30534  gsumpart  30740  gsumhashmul  30741  gsumle  30775  locfinreflem  31193  sibfof  31708  sitgclbn  31711  sitgaddlemb  31716  eulerpartlemgu  31745  ballotlemsima  31883  reprinrn  31999  bnj1311  32406  fnrelpredd  32472  erdsze2lem2  32564  iccllysconn  32610  cvmopnlem  32638  msrf  32902  frpomin  33191  frrlem4  33239  frrlem13  33248  fprlem1  33250  frrlem15  33255  nosupno  33316  neiin  33793  neibastop1  33820  neibastop2lem  33821  topmeet  33825  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem19  35076  poimirlem30  35087  cnambfre  35105  itg2gt0cn  35112  sstotbnd2  35212  sstotbnd3  35214  ssbnd  35226  ismtyima  35241  heibor1lem  35247  idresssidinxp  35726  pmodlem2  37143  pmodN  37146  diaintclN  38354  djaclN  38432  dibintclN  38463  dicval  38472  dihoml4c  38672  djhcl  38696  isnacs2  39647  isnacs3  39651  diophrw  39700  pellfundre  39822  pellfundge  39823  pellfundlb  39825  pellfundglb  39826  fnwe2lem2  39995  lmhmfgima  40028  hbt  40074  cnvtrcl0  40326  trclrelexplem  40412  relexp0a  40417  isotone2  40752  imo72b2lem1  40874  climinf  42248  islptre  42261  limccog  42262  limcleqr  42286  itgcoscmulx  42611  ismbl3  42628  ismbl4  42635  stoweidlem27  42669  dirkercncflem2  42746  fourierdlem38  42787  fourierdlem49  42797  fourierdlem51  42799  fourierdlem54  42802  fourierdlem63  42811  fourierdlem68  42816  fourierdlem69  42817  fourierdlem70  42818  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem80  42828  fourierdlem84  42832  fourierdlem85  42833  fourierdlem88  42836  fourierdlem100  42848  fourierdlem101  42849  fourierdlem104  42852  fourierdlem107  42855  fourierdlem111  42859  fourierdlem112  42860  caragenel2d  43171  hoidmv1lelem3  43232  hspmbllem3  43267  sssmf  43372  smfrec  43421  smfsuplem1  43442  mgmhmima  44422