Theorem sstrid 4020

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

Syntax hints:   → wi 4   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3993

This theorem is referenced by:  difsymssdifssd  4283  wereu2  5697  sofld  6218  resssxp  6301  frpomin  6372  fimass  6767  fvmptss  7041  fimacnvOLD  7104  isofr2  7380  frxp  8167  fnse  8174  frxp2  8185  frxp3  8192  frrlem4  8330  frrlem13  8339  fprlem1  8341  smores2  8410  naddunif  8749  dffi3  9500  marypha1lem  9502  ordtypelem7  9593  ordtypelem8  9594  oismo  9609  unxpwdom2  9657  cantnfres  9746  oemapvali  9753  frmin  9818  frrlem15  9826  frrlem16  9827  tskwe  10019  acndom2  10123  dfac2a  10199  dfac12lem2  10214  cfle  10323  cofsmo  10338  coftr  10342  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  enfin1ai  10453  fin1a2lem12  10480  ttukeylem7  10584  alephexp1  10648  fpwwe2lem12  10711  fpwwe2  10712  canth4  10716  canthwelem  10719  pwfseqlem1  10727  pwfseqlem4  10731  fzossnn0  13747  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  xptrrel  15029  limsupgle  15523  limsupgre  15527  rlimres  15604  lo1res  15605  lo1resb  15610  rlimresb  15611  o1resb  15612  o1of2  15659  o1rlimmul  15665  isercolllem2  15714  isercoll  15716  climsup  15718  fprodntriv  15990  bitsinvp1  16495  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadasslem  16516  sadeq  16518  bitsres  16519  smuval2  16528  smupval  16534  smueqlem  16536  smumul  16539  1arith  16974  isstruct2  17196  setscom  17227  ressress  17307  imasvscafn  17597  imasless  17600  mrcssv  17672  isacs1i  17715  mreacs  17716  acsfn  17717  isacs4lem  18614  isacs5lem  18615  mgmhmima  18753  mhmima  18860  cntzmhm  19381  f1omvdconj  19488  f1omvdco2  19490  symgsssg  19509  symggen  19512  efgval  19759  gsumzaddlem  19963  gsumconst  19976  dmdprdd  20043  dprdfeq0  20066  dprdres  20072  dprdss  20073  dprdz  20074  subgdmdprd  20078  dprddisj2  20083  dprd2dlem1  20085  dprd2da  20086  dprd2d2  20088  dmdprdsplit2lem  20089  lmhmlsp  21071  lsppratlem4  21175  islbs3  21180  lbsextlem3  21185  znleval  21596  evpmss  21627  frlmsslsp  21839  lindff1  21863  lindfrn  21864  f1lindf  21865  lindfmm  21870  lsslindf  21873  mplcoe5  22081  mplind  22117  basdif0  22981  tgcl  22997  ppttop  23035  epttop  23037  ntrin  23090  mretopd  23121  neiptoptop  23160  cnclsi  23301  cnconst2  23312  cnrest2  23315  cnpresti  23317  cnprest2  23319  fiuncmp  23433  connsub  23450  connima  23454  iunconnlem  23456  1stcfb  23474  2ndc1stc  23480  2ndcdisj  23485  kgentopon  23567  llycmpkgen2  23579  1stckgenlem  23582  kgencn3  23587  ptclsg  23644  ptcnplem  23650  txtube  23669  hausdiag  23674  txkgen  23681  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  qtoptop2  23728  basqtop  23740  imastopn  23749  hmeores  23800  hmphdis  23825  ptcmpfi  23842  fbssfi  23866  filin  23883  infil  23892  fgtr  23919  elfm  23976  hausflim  24010  flimclslem  24013  fclscmp  24059  cnextcn  24096  tmdgsum2  24125  tgpconncomp  24142  ustexsym  24245  ustund  24251  ustimasn  24258  utoptop  24264  utopbas  24265  restutopopn  24268  blin2  24460  metustexhalf  24590  icccmplem2  24864  icccmplem3  24865  reconnlem2  24868  tcphcph  25290  fmcfil  25325  resscdrg  25411  ivthlem2  25506  ivthlem3  25507  ivth2  25509  ovolfiniun  25555  ovoliunlem1  25556  ismbl2  25581  nulmbl2  25590  unmbl  25591  shftmbl  25592  voliunlem1  25604  voliunlem2  25605  ioombl1lem4  25615  uniioombllem4  25640  uniioombllem5  25641  dyadmbllem  25653  dyadmbl  25654  mbflimsup  25720  i1fima  25732  i1fima2  25733  i1fadd  25749  itg1addlem4  25753  itg1addlem4OLD  25754  itg2splitlem  25803  itg2split  25804  ellimc3  25934  limcflflem  25935  limcflf  25936  limcresi  25940  limciun  25949  dvreslem  25964  dvres2lem  25965  dvres  25966  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvlip  26052  dvlip2  26054  c1liplem1  26055  dvivthlem1  26067  dvne0  26070  lhop1lem  26072  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubstlem  26109  mdegleb  26123  mdeglt  26124  mdegldg  26125  mdegxrcl  26126  mdegcl  26128  ig1peu  26234  reeff1olem  26508  logccv  26723  rlimcnp2  27027  lgamgulmlem2  27091  ppisval  27165  prmdvdsfi  27168  mumul  27242  sqff1o  27243  chtlepsi  27268  chpub  27282  dchrisum0lem2a  27579  pntlem3  27671  nosupno  27766  noetalem1  27804  cutlt  27984  negsproplem2  28079  ex-res  30473  htthlem  30949  chlejb1i  31508  ssmd2  32344  fz2ssnn0  32790  gsumpart  33038  gsumhashmul  33040  gsumle  33074  locfinreflem  33786  sibfof  34305  sitgclbn  34308  sitgaddlemb  34313  eulerpartlemgu  34342  ballotlemsima  34480  reprinrn  34595  bnj1311  35000  fnrelpredd  35065  erdsze2lem2  35172  iccllysconn  35218  cvmopnlem  35246  msrf  35510  neiin  36298  neibastop1  36325  neibastop2lem  36326  topmeet  36330  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem19  37599  poimirlem30  37610  cnambfre  37628  itg2gt0cn  37635  sstotbnd2  37734  sstotbnd3  37736  ssbnd  37748  ismtyima  37763  heibor1lem  37769  idresssidinxp  38264  pmodlem2  39804  pmodN  39807  diaintclN  41015  djaclN  41093  dibintclN  41124  dicval  41133  dihoml4c  41333  djhcl  41357  infdesc  42598  isnacs2  42662  isnacs3  42666  diophrw  42715  pellfundre  42837  pellfundge  42838  pellfundlb  42840  pellfundglb  42841  fnwe2lem2  43008  lmhmfgima  43041  hbt  43087  omabs2  43294  nadd2rabord  43347  nadd1rabord  43351  cnvtrcl0  43588  trclrelexplem  43673  relexp0a  43678  isotone2  44011  imo72b2lem1  44131  climinf  45527  islptre  45540  limccog  45541  limcleqr  45565  itgcoscmulx  45890  ismbl3  45907  ismbl4  45914  stoweidlem27  45948  dirkercncflem2  46025  fourierdlem38  46066  fourierdlem49  46076  fourierdlem51  46078  fourierdlem54  46081  fourierdlem63  46090  fourierdlem68  46095  fourierdlem69  46096  fourierdlem70  46097  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem100  46127  fourierdlem101  46128  fourierdlem104  46131  fourierdlem107  46134  fourierdlem111  46138  fourierdlem112  46139  caragenel2d  46453  hoidmv1lelem3  46514  hspmbllem3  46549  sssmf  46659  smfrec  46710  smfsuplem1  46732