Theorem sstrid 3991

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

Syntax hints:   → wi 4   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  difsymssdifssd  4254  wereu2  5675  sofld  6191  resssxp  6274  frpomin  6346  fimass  6743  fvmptss  7017  fimacnvOLD  7080  isofr2  7352  frxp  8131  fnse  8138  frxp2  8149  frxp3  8156  frrlem4  8294  frrlem13  8303  fprlem1  8305  smores2  8374  naddunif  8713  dffi3  9454  marypha1lem  9456  ordtypelem7  9547  ordtypelem8  9548  oismo  9563  unxpwdom2  9611  cantnfres  9700  oemapvali  9707  frmin  9772  frrlem15  9780  frrlem16  9781  tskwe  9973  acndom2  10077  dfac2a  10152  dfac12lem2  10167  cfle  10277  cofsmo  10292  coftr  10296  isf34lem5  10401  isf34lem7  10402  isf34lem6  10403  enfin1ai  10407  fin1a2lem12  10434  ttukeylem7  10538  alephexp1  10602  fpwwe2lem12  10665  fpwwe2  10666  canth4  10670  canthwelem  10673  pwfseqlem1  10681  pwfseqlem4  10685  fzossnn0  13695  fsuppmapnn0fiublem  13987  fsuppmapnn0fiub  13988  xptrrel  14959  limsupgle  15453  limsupgre  15457  rlimres  15534  lo1res  15535  lo1resb  15540  rlimresb  15541  o1resb  15542  o1of2  15589  o1rlimmul  15595  isercolllem2  15644  isercoll  15646  climsup  15648  fprodntriv  15918  bitsinvp1  16423  sadcaddlem  16431  sadadd2lem  16433  sadadd3  16435  sadasslem  16444  sadeq  16446  bitsres  16447  smuval2  16456  smupval  16462  smueqlem  16464  smumul  16467  1arith  16895  isstruct2  17117  setscom  17148  ressress  17228  imasvscafn  17518  imasless  17521  mrcssv  17593  isacs1i  17636  mreacs  17637  acsfn  17638  isacs4lem  18535  isacs5lem  18536  mgmhmima  18674  mhmima  18776  cntzmhm  19291  f1omvdconj  19400  f1omvdco2  19402  symgsssg  19421  symggen  19424  efgval  19671  gsumzaddlem  19875  gsumconst  19888  dmdprdd  19955  dprdfeq0  19978  dprdres  19984  dprdss  19985  dprdz  19986  subgdmdprd  19990  dprddisj2  19995  dprd2dlem1  19997  dprd2da  19998  dprd2d2  20000  dmdprdsplit2lem  20001  lmhmlsp  20933  lsppratlem4  21037  islbs3  21042  lbsextlem3  21047  znleval  21487  evpmss  21517  frlmsslsp  21729  lindff1  21753  lindfrn  21754  f1lindf  21755  lindfmm  21760  lsslindf  21763  mplcoe5  21977  mplind  22013  basdif0  22855  tgcl  22871  ppttop  22909  epttop  22911  ntrin  22964  mretopd  22995  neiptoptop  23034  cnclsi  23175  cnconst2  23186  cnrest2  23189  cnpresti  23191  cnprest2  23193  fiuncmp  23307  connsub  23324  connima  23328  iunconnlem  23330  1stcfb  23348  2ndc1stc  23354  2ndcdisj  23359  kgentopon  23441  llycmpkgen2  23453  1stckgenlem  23456  kgencn3  23461  ptclsg  23518  ptcnplem  23524  txtube  23543  hausdiag  23548  txkgen  23555  xkoco1cn  23560  xkoco2cn  23561  xkococnlem  23562  qtoptop2  23602  basqtop  23614  imastopn  23623  hmeores  23674  hmphdis  23699  ptcmpfi  23716  fbssfi  23740  filin  23757  infil  23766  fgtr  23793  elfm  23850  hausflim  23884  flimclslem  23887  fclscmp  23933  cnextcn  23970  tmdgsum2  23999  tgpconncomp  24016  ustexsym  24119  ustund  24125  ustimasn  24132  utoptop  24138  utopbas  24139  restutopopn  24142  blin2  24334  metustexhalf  24464  icccmplem2  24738  icccmplem3  24739  reconnlem2  24742  tcphcph  25164  fmcfil  25199  resscdrg  25285  ivthlem2  25380  ivthlem3  25381  ivth2  25383  ovolfiniun  25429  ovoliunlem1  25430  ismbl2  25455  nulmbl2  25464  unmbl  25465  shftmbl  25466  voliunlem1  25478  voliunlem2  25479  ioombl1lem4  25489  uniioombllem4  25514  uniioombllem5  25515  dyadmbllem  25527  dyadmbl  25528  mbflimsup  25594  i1fima  25606  i1fima2  25607  i1fadd  25623  itg1addlem4  25627  itg1addlem4OLD  25628  itg2splitlem  25677  itg2split  25678  ellimc3  25807  limcflflem  25808  limcflf  25809  limcresi  25813  limciun  25822  dvreslem  25837  dvres2lem  25838  dvres  25839  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvlip  25925  dvlip2  25927  c1liplem1  25928  dvivthlem1  25940  dvne0  25943  lhop1lem  25945  lhop  25948  dvcnvrelem1  25949  dvcnvrelem2  25950  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  itgsubstlem  25982  mdegleb  25999  mdeglt  26000  mdegldg  26001  mdegxrcl  26002  mdegcl  26004  ig1peu  26108  reeff1olem  26382  logccv  26596  rlimcnp2  26897  lgamgulmlem2  26961  ppisval  27035  prmdvdsfi  27038  mumul  27112  sqff1o  27113  chtlepsi  27138  chpub  27152  dchrisum0lem2a  27449  pntlem3  27541  nosupno  27635  noetalem1  27673  cutlt  27851  negsproplem2  27940  ex-res  30250  htthlem  30726  chlejb1i  31285  ssmd2  32121  fz2ssnn0  32553  gsumpart  32769  gsumhashmul  32770  gsumle  32804  locfinreflem  33441  sibfof  33960  sitgclbn  33963  sitgaddlemb  33968  eulerpartlemgu  33997  ballotlemsima  34135  reprinrn  34250  bnj1311  34655  fnrelpredd  34712  erdsze2lem2  34814  iccllysconn  34860  cvmopnlem  34888  msrf  35152  neiin  35816  neibastop1  35843  neibastop2lem  35844  topmeet  35848  poimirlem1  37094  poimirlem2  37095  poimirlem3  37096  poimirlem11  37104  poimirlem12  37105  poimirlem16  37109  poimirlem19  37112  poimirlem30  37123  cnambfre  37141  itg2gt0cn  37148  sstotbnd2  37247  sstotbnd3  37249  ssbnd  37261  ismtyima  37276  heibor1lem  37282  idresssidinxp  37780  pmodlem2  39320  pmodN  39323  diaintclN  40531  djaclN  40609  dibintclN  40640  dicval  40649  dihoml4c  40849  djhcl  40873  infdesc  42067  isnacs2  42126  isnacs3  42130  diophrw  42179  pellfundre  42301  pellfundge  42302  pellfundlb  42304  pellfundglb  42305  fnwe2lem2  42475  lmhmfgima  42508  hbt  42554  omabs2  42761  nadd2rabord  42814  nadd1rabord  42818  cnvtrcl0  43056  trclrelexplem  43141  relexp0a  43146  isotone2  43479  imo72b2lem1  43599  climinf  44994  islptre  45007  limccog  45008  limcleqr  45032  itgcoscmulx  45357  ismbl3  45374  ismbl4  45381  stoweidlem27  45415  dirkercncflem2  45492  fourierdlem38  45533  fourierdlem49  45543  fourierdlem51  45545  fourierdlem54  45548  fourierdlem63  45557  fourierdlem68  45562  fourierdlem69  45563  fourierdlem70  45564  fourierdlem74  45568  fourierdlem75  45569  fourierdlem76  45570  fourierdlem80  45574  fourierdlem84  45578  fourierdlem85  45579  fourierdlem88  45582  fourierdlem100  45594  fourierdlem101  45595  fourierdlem104  45598  fourierdlem107  45601  fourierdlem111  45605  fourierdlem112  45606  caragenel2d  45920  hoidmv1lelem3  45981  hspmbllem3  46016  sssmf  46126  smfrec  46177  smfsuplem1  46199