Theorem sstrid 3949

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

Syntax hints:   → wi 4   ⊆ wss 3906

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3923

This theorem is referenced by:  difsymssdifssd  4218  wereu2  5660  sofld  6187  resssxp  6273  frpomin  6343  fimass  6728  fvmptss  7004  isofr2  7344  frxp  8123  fnse  8130  frxp2  8141  frxp3  8148  frrlem4  8287  frrlem13  8296  fprlem1  8298  smores2  8342  naddunif  8681  dffi3  9392  marypha1lem  9394  ordtypelem7  9487  ordtypelem8  9488  oismo  9503  unxpwdom2  9551  cantnfres  9647  oemapvali  9654  frmin  9722  frrlem15  9730  frrlem16  9731  tskwe  9937  acndom2  10039  dfac2a  10114  dfac12lem2  10129  cfle  10238  cofsmo  10254  coftr  10258  isf34lem5  10363  isf34lem7  10364  isf34lem6  10365  enfin1ai  10369  fin1a2lem12  10396  ttukeylem7  10500  alephexp1  10565  fpwwe2lem12  10628  fpwwe2  10629  canth4  10633  canthwelem  10636  pwfseqlem1  10644  pwfseqlem4  10648  fzossnn0  13721  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  xptrrel  15019  limsupgle  15530  limsupgre  15534  rlimres  15611  lo1res  15612  lo1resb  15617  rlimresb  15618  o1resb  15619  o1of2  15666  o1rlimmul  15672  isercolllem2  15719  isercoll  15721  climsup  15723  fprodntriv  15998  bitsinvp1  16508  sadcaddlem  16516  sadadd2lem  16518  sadadd3  16520  sadasslem  16529  sadeq  16531  bitsres  16532  smuval2  16541  smupval  16547  smueqlem  16549  smumul  16552  1arith  16988  isstruct2  17210  setscom  17241  ressress  17308  imasvscafn  17592  imasless  17595  mrcssv  17671  isacs1i  17714  mreacs  17715  acsfn  17716  isacs4lem  18601  isacs5lem  18602  mgmhmima  18774  mhmima  18885  cntzmhm  19412  f1omvdconj  19517  f1omvdco2  19519  symgsssg  19538  symggen  19541  efgval  19788  gsumzaddlem  19992  gsumconst  20005  dmdprdd  20072  dprdfeq0  20095  dprdres  20101  dprdss  20102  dprdz  20103  subgdmdprd  20107  dprddisj2  20112  dprd2dlem1  20114  dprd2da  20115  dprd2d2  20117  dmdprdsplit2lem  20118  gsumle  20216  lmhmlsp  21151  lsppratlem4  21255  islbs3  21260  lbsextlem3  21265  znleval  21685  evpmss  21717  frlmsslsp  21927  lindff1  21951  lindfrn  21952  f1lindf  21953  lindfmm  21958  lsslindf  21961  mplcoe5  22172  mplind  22202  basdif0  23091  tgcl  23107  ppttop  23145  epttop  23147  ntrin  23199  mretopd  23230  neiptoptop  23269  cnclsi  23410  cnconst2  23421  cnrest2  23424  cnpresti  23426  cnprest2  23428  fiuncmp  23542  connsub  23559  connima  23563  iunconnlem  23565  1stcfb  23583  2ndc1stc  23589  2ndcdisj  23594  kgentopon  23676  llycmpkgen2  23688  1stckgenlem  23691  kgencn3  23696  ptclsg  23753  ptcnplem  23759  txtube  23778  hausdiag  23783  txkgen  23790  xkoco1cn  23795  xkoco2cn  23796  xkococnlem  23797  qtoptop2  23837  basqtop  23849  imastopn  23858  hmeores  23909  hmphdis  23934  ptcmpfi  23951  fbssfi  23975  filin  23992  infil  24001  fgtr  24028  elfm  24085  hausflim  24119  flimclslem  24122  fclscmp  24168  cnextcn  24205  tmdgsum2  24234  tgpconncomp  24251  ustexsym  24354  ustund  24360  ustimasn  24366  utoptop  24372  utopbas  24373  restutopopn  24376  blin2  24567  metustexhalf  24694  icccmplem2  24962  icccmplem3  24963  reconnlem2  24966  tcphcph  25377  fmcfil  25412  resscdrg  25498  ivthlem2  25592  ivthlem3  25593  ivth2  25595  ovolfiniun  25641  ovoliunlem1  25642  ismbl2  25667  nulmbl2  25676  unmbl  25677  shftmbl  25678  voliunlem1  25690  voliunlem2  25691  ioombl1lem4  25701  uniioombllem4  25726  uniioombllem5  25727  dyadmbllem  25739  dyadmbl  25740  mbflimsup  25806  i1fima  25818  i1fima2  25819  i1fadd  25835  itg1addlem4  25839  itg2splitlem  25888  itg2split  25889  ellimc3  26019  limcflflem  26020  limcflf  26021  limcresi  26025  limciun  26034  dvreslem  26049  dvres2lem  26050  dvres  26051  dvaddbr  26078  dvmulbr  26079  dvlip  26133  dvlip2  26135  c1liplem1  26136  dvivthlem1  26148  dvne0  26151  lhop1lem  26153  lhop  26156  dvcnvrelem1  26157  dvcnvrelem2  26158  dvfsumle  26161  dvfsumabs  26163  dvfsumlem2  26167  itgsubstlem  26188  mdegleb  26202  mdeglt  26203  mdegldg  26204  mdegxrcl  26205  mdegcl  26207  ig1peu  26313  reeff1olem  26590  logccv  26809  rlimcnp2  27112  lgamgulmlem2  27175  ppisval  27249  prmdvdsfi  27252  mumul  27326  sqff1o  27327  chtlepsi  27351  chpub  27365  dchrisum0lem2a  27662  pntlem3  27754  nosupno  27848  noetalem1  27886  cutlt  28106  negsproplem2  28203  onsbnd  28455  ex-res  30773  htthlem  31250  chlejb1i  31809  ssmd2  32645  fz2ssnn0  33111  gsumpart  33364  gsumhashmul  33368  elrgspnsubrunlem2  33549  extvfvcl  33907  mplvrpmrhm  33918  esplyind  33946  vietalem  33950  locfinreflem  34211  sibfof  34711  sitgclbn  34714  sitgaddlemb  34719  eulerpartlemgu  34748  ballotlemsima  34887  reprinrn  34986  bnj1311  35393  fnrelpredd  35463  erdsze2lem2  35677  iccllysconn  35723  cvmopnlem  35751  msrf  36015  neiin  36824  neibastop1  36851  neibastop2lem  36852  topmeet  36856  ttciunun  37003  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem11  38263  poimirlem12  38264  poimirlem16  38268  poimirlem19  38271  poimirlem30  38282  cnambfre  38300  itg2gt0cn  38307  sstotbnd2  38406  sstotbnd3  38408  ssbnd  38420  ismtyima  38435  heibor1lem  38441  idresssidinxp  38944  pmodlem2  40602  pmodN  40605  diaintclN  41813  djaclN  41891  dibintclN  41922  dicval  41931  dihoml4c  42131  djhcl  42155  infdesc  43358  isnacs2  43420  isnacs3  43424  diophrw  43473  pellfundre  43591  pellfundge  43592  pellfundlb  43594  pellfundglb  43595  fnwe2lem2  43761  lmhmfgima  43794  hbt  43840  omabs2  44042  nadd2rabord  44095  nadd1rabord  44099  cnvtrcl0  44335  trclrelexplem  44420  relexp0a  44425  isotone2  44758  imo72b2lem1  44878  tcfr  45655  modelaxreplem1  45670  wfac8prim  45694  climinf  46305  islptre  46318  limccog  46319  limcleqr  46341  limsupvaluz2  46435  itgcoscmulx  46666  ismbl3  46683  ismbl4  46690  stoweidlem27  46724  dirkercncflem2  46801  fourierdlem38  46842  fourierdlem51  46854  fourierdlem54  46857  fourierdlem63  46866  fourierdlem68  46871  fourierdlem69  46872  fourierdlem70  46873  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem80  46883  fourierdlem84  46887  fourierdlem85  46888  fourierdlem88  46891  fourierdlem100  46903  fourierdlem101  46904  fourierdlem104  46907  fourierdlem107  46910  fourierdlem111  46914  fourierdlem112  46915  caragenel2d  47229  hoidmv1lelem3  47290  hspmbllem3  47325  sssmf  47435  smfrec  47486  smfsuplem1  47508