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

Syntax hints:   → wi 4   ⊆ wss 3898

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

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

This theorem is referenced by:  difsymssdifssd  4213  wereu2  5616  sofld  6139  resssxp  6222  frpomin  6292  fimass  6676  fvmptss  6947  isofr2  7284  frxp  8062  fnse  8069  frxp2  8080  frxp3  8087  frrlem4  8225  frrlem13  8234  fprlem1  8236  smores2  8280  naddunif  8614  dffi3  9322  marypha1lem  9324  ordtypelem7  9417  ordtypelem8  9418  oismo  9433  unxpwdom2  9481  cantnfres  9574  oemapvali  9581  frmin  9649  frrlem15  9657  frrlem16  9658  tskwe  9850  acndom2  9952  dfac2a  10028  dfac12lem2  10043  cfle  10152  cofsmo  10167  coftr  10171  isf34lem5  10276  isf34lem7  10277  isf34lem6  10278  enfin1ai  10282  fin1a2lem12  10309  ttukeylem7  10413  alephexp1  10477  fpwwe2lem12  10540  fpwwe2  10541  canth4  10545  canthwelem  10548  pwfseqlem1  10556  pwfseqlem4  10560  fzossnn0  13592  fsuppmapnn0fiublem  13899  fsuppmapnn0fiub  13900  xptrrel  14889  limsupgle  15386  limsupgre  15390  rlimres  15467  lo1res  15468  lo1resb  15473  rlimresb  15474  o1resb  15475  o1of2  15522  o1rlimmul  15528  isercolllem2  15575  isercoll  15577  climsup  15579  fprodntriv  15851  bitsinvp1  16362  sadcaddlem  16370  sadadd2lem  16372  sadadd3  16374  sadasslem  16383  sadeq  16385  bitsres  16386  smuval2  16395  smupval  16401  smueqlem  16403  smumul  16406  1arith  16841  isstruct2  17062  setscom  17093  ressress  17160  imasvscafn  17443  imasless  17446  mrcssv  17522  isacs1i  17565  mreacs  17566  acsfn  17567  isacs4lem  18452  isacs5lem  18453  mgmhmima  18625  mhmima  18735  cntzmhm  19255  f1omvdconj  19360  f1omvdco2  19362  symgsssg  19381  symggen  19384  efgval  19631  gsumzaddlem  19835  gsumconst  19848  dmdprdd  19915  dprdfeq0  19938  dprdres  19944  dprdss  19945  dprdz  19946  subgdmdprd  19950  dprddisj2  19955  dprd2dlem1  19957  dprd2da  19958  dprd2d2  19960  dmdprdsplit2lem  19961  gsumle  20059  lmhmlsp  20985  lsppratlem4  21089  islbs3  21094  lbsextlem3  21099  znleval  21493  evpmss  21525  frlmsslsp  21735  lindff1  21759  lindfrn  21760  f1lindf  21761  lindfmm  21766  lsslindf  21769  mplcoe5  21976  mplind  22006  basdif0  22869  tgcl  22885  ppttop  22923  epttop  22925  ntrin  22977  mretopd  23008  neiptoptop  23047  cnclsi  23188  cnconst2  23199  cnrest2  23202  cnpresti  23204  cnprest2  23206  fiuncmp  23320  connsub  23337  connima  23341  iunconnlem  23343  1stcfb  23361  2ndc1stc  23367  2ndcdisj  23372  kgentopon  23454  llycmpkgen2  23466  1stckgenlem  23469  kgencn3  23474  ptclsg  23531  ptcnplem  23537  txtube  23556  hausdiag  23561  txkgen  23568  xkoco1cn  23573  xkoco2cn  23574  xkococnlem  23575  qtoptop2  23615  basqtop  23627  imastopn  23636  hmeores  23687  hmphdis  23712  ptcmpfi  23729  fbssfi  23753  filin  23770  infil  23779  fgtr  23806  elfm  23863  hausflim  23897  flimclslem  23900  fclscmp  23946  cnextcn  23983  tmdgsum2  24012  tgpconncomp  24029  ustexsym  24132  ustund  24138  ustimasn  24144  utoptop  24150  utopbas  24151  restutopopn  24154  blin2  24345  metustexhalf  24472  icccmplem2  24740  icccmplem3  24741  reconnlem2  24744  tcphcph  25165  fmcfil  25200  resscdrg  25286  ivthlem2  25381  ivthlem3  25382  ivth2  25384  ovolfiniun  25430  ovoliunlem1  25431  ismbl2  25456  nulmbl2  25465  unmbl  25466  shftmbl  25467  voliunlem1  25479  voliunlem2  25480  ioombl1lem4  25490  uniioombllem4  25515  uniioombllem5  25516  dyadmbllem  25528  dyadmbl  25529  mbflimsup  25595  i1fima  25607  i1fima2  25608  i1fadd  25624  itg1addlem4  25628  itg2splitlem  25677  itg2split  25678  ellimc3  25808  limcflflem  25809  limcflf  25810  limcresi  25814  limciun  25823  dvreslem  25838  dvres2lem  25839  dvres  25840  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvlip  25926  dvlip2  25928  c1liplem1  25929  dvivthlem1  25941  dvne0  25944  lhop1lem  25946  lhop  25949  dvcnvrelem1  25950  dvcnvrelem2  25951  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  itgsubstlem  25983  mdegleb  25997  mdeglt  25998  mdegldg  25999  mdegxrcl  26000  mdegcl  26002  ig1peu  26108  reeff1olem  26384  logccv  26600  rlimcnp2  26904  lgamgulmlem2  26968  ppisval  27042  prmdvdsfi  27045  mumul  27119  sqff1o  27120  chtlepsi  27145  chpub  27159  dchrisum0lem2a  27456  pntlem3  27548  nosupno  27643  noetalem1  27681  cutlt  27877  negsproplem2  27972  ex-res  30423  htthlem  30899  chlejb1i  31458  ssmd2  32294  fz2ssnn0  32772  gsumpart  33044  gsumhashmul  33048  elrgspnsubrunlem2  33222  extvfvcl  33587  mplvrpmrhm  33595  esplyind  33613  locfinreflem  33874  sibfof  34374  sitgclbn  34377  sitgaddlemb  34382  eulerpartlemgu  34411  ballotlemsima  34550  reprinrn  34652  bnj1311  35057  fnrelpredd  35123  erdsze2lem2  35269  iccllysconn  35315  cvmopnlem  35343  msrf  35607  neiin  36397  neibastop1  36424  neibastop2lem  36425  topmeet  36429  poimirlem1  37682  poimirlem2  37683  poimirlem3  37684  poimirlem11  37692  poimirlem12  37693  poimirlem16  37697  poimirlem19  37700  poimirlem30  37711  cnambfre  37729  itg2gt0cn  37736  sstotbnd2  37835  sstotbnd3  37837  ssbnd  37849  ismtyima  37864  heibor1lem  37870  idresssidinxp  38367  pmodlem2  39967  pmodN  39970  diaintclN  41178  djaclN  41256  dibintclN  41287  dicval  41296  dihoml4c  41496  djhcl  41520  infdesc  42762  isnacs2  42824  isnacs3  42828  diophrw  42877  pellfundre  42999  pellfundge  43000  pellfundlb  43002  pellfundglb  43003  fnwe2lem2  43169  lmhmfgima  43202  hbt  43248  omabs2  43450  nadd2rabord  43503  nadd1rabord  43507  cnvtrcl0  43744  trclrelexplem  43829  relexp0a  43834  isotone2  44167  imo72b2lem1  44287  tcfr  45081  modelaxreplem1  45096  wfac8prim  45120  climinf  45731  islptre  45744  limccog  45745  limcleqr  45767  limsupvaluz2  45861  itgcoscmulx  46092  ismbl3  46109  ismbl4  46116  stoweidlem27  46150  dirkercncflem2  46227  fourierdlem38  46268  fourierdlem49  46278  fourierdlem51  46280  fourierdlem54  46283  fourierdlem63  46292  fourierdlem68  46297  fourierdlem69  46298  fourierdlem70  46299  fourierdlem74  46303  fourierdlem75  46304  fourierdlem76  46305  fourierdlem80  46309  fourierdlem84  46313  fourierdlem85  46314  fourierdlem88  46317  fourierdlem100  46329  fourierdlem101  46330  fourierdlem104  46333  fourierdlem107  46336  fourierdlem111  46340  fourierdlem112  46341  caragenel2d  46655  hoidmv1lelem3  46716  hspmbllem3  46751  sssmf  46861  smfrec  46912  smfsuplem1  46934