Theorem sstrid 3933

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

Syntax hints:   → wi 4   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3907

This theorem is referenced by:  difsymssdifssd  4199  wereu2  5622  sofld  6145  resssxp  6228  frpomin  6298  fimass  6682  fvmptss  6955  isofr2  7295  frxp  8073  fnse  8080  frxp2  8091  frxp3  8098  frrlem4  8236  frrlem13  8245  fprlem1  8247  smores2  8291  naddunif  8626  dffi3  9341  marypha1lem  9343  ordtypelem7  9436  ordtypelem8  9437  oismo  9452  unxpwdom2  9500  cantnfres  9596  oemapvali  9603  frmin  9671  frrlem15  9679  frrlem16  9680  tskwe  9872  acndom2  9974  dfac2a  10050  dfac12lem2  10065  cfle  10174  cofsmo  10189  coftr  10193  isf34lem5  10298  isf34lem7  10299  isf34lem6  10300  enfin1ai  10304  fin1a2lem12  10331  ttukeylem7  10435  alephexp1  10500  fpwwe2lem12  10563  fpwwe2  10564  canth4  10568  canthwelem  10571  pwfseqlem1  10579  pwfseqlem4  10583  fzossnn0  13643  fsuppmapnn0fiublem  13950  fsuppmapnn0fiub  13951  xptrrel  14940  limsupgle  15437  limsupgre  15441  rlimres  15518  lo1res  15519  lo1resb  15524  rlimresb  15525  o1resb  15526  o1of2  15573  o1rlimmul  15579  isercolllem2  15626  isercoll  15628  climsup  15630  fprodntriv  15905  bitsinvp1  16416  sadcaddlem  16424  sadadd2lem  16426  sadadd3  16428  sadasslem  16437  sadeq  16439  bitsres  16440  smuval2  16449  smupval  16455  smueqlem  16457  smumul  16460  1arith  16896  isstruct2  17117  setscom  17148  ressress  17215  imasvscafn  17499  imasless  17502  mrcssv  17578  isacs1i  17621  mreacs  17622  acsfn  17623  isacs4lem  18508  isacs5lem  18509  mgmhmima  18681  mhmima  18791  cntzmhm  19314  f1omvdconj  19419  f1omvdco2  19421  symgsssg  19440  symggen  19443  efgval  19690  gsumzaddlem  19894  gsumconst  19907  dmdprdd  19974  dprdfeq0  19997  dprdres  20003  dprdss  20004  dprdz  20005  subgdmdprd  20009  dprddisj2  20014  dprd2dlem1  20016  dprd2da  20017  dprd2d2  20019  dmdprdsplit2lem  20020  gsumle  20118  lmhmlsp  21046  lsppratlem4  21150  islbs3  21155  lbsextlem3  21160  znleval  21536  evpmss  21568  frlmsslsp  21778  lindff1  21802  lindfrn  21803  f1lindf  21804  lindfmm  21809  lsslindf  21812  mplcoe5  22023  mplind  22053  basdif0  22943  tgcl  22959  ppttop  22997  epttop  22999  ntrin  23051  mretopd  23082  neiptoptop  23121  cnclsi  23262  cnconst2  23273  cnrest2  23276  cnpresti  23278  cnprest2  23280  fiuncmp  23394  connsub  23411  connima  23415  iunconnlem  23417  1stcfb  23435  2ndc1stc  23441  2ndcdisj  23446  kgentopon  23528  llycmpkgen2  23540  1stckgenlem  23543  kgencn3  23548  ptclsg  23605  ptcnplem  23611  txtube  23630  hausdiag  23635  txkgen  23642  xkoco1cn  23647  xkoco2cn  23648  xkococnlem  23649  qtoptop2  23689  basqtop  23701  imastopn  23710  hmeores  23761  hmphdis  23786  ptcmpfi  23803  fbssfi  23827  filin  23844  infil  23853  fgtr  23880  elfm  23937  hausflim  23971  flimclslem  23974  fclscmp  24020  cnextcn  24057  tmdgsum2  24086  tgpconncomp  24103  ustexsym  24206  ustund  24212  ustimasn  24218  utoptop  24224  utopbas  24225  restutopopn  24228  blin2  24419  metustexhalf  24546  icccmplem2  24814  icccmplem3  24815  reconnlem2  24818  tcphcph  25229  fmcfil  25264  resscdrg  25350  ivthlem2  25444  ivthlem3  25445  ivth2  25447  ovolfiniun  25493  ovoliunlem1  25494  ismbl2  25519  nulmbl2  25528  unmbl  25529  shftmbl  25530  voliunlem1  25542  voliunlem2  25543  ioombl1lem4  25553  uniioombllem4  25578  uniioombllem5  25579  dyadmbllem  25591  dyadmbl  25592  mbflimsup  25658  i1fima  25670  i1fima2  25671  i1fadd  25687  itg1addlem4  25691  itg2splitlem  25740  itg2split  25741  ellimc3  25871  limcflflem  25872  limcflf  25873  limcresi  25877  limciun  25886  dvreslem  25901  dvres2lem  25902  dvres  25903  dvaddbr  25930  dvmulbr  25931  dvlip  25985  dvlip2  25987  c1liplem1  25988  dvivthlem1  26000  dvne0  26003  lhop1lem  26005  lhop  26008  dvcnvrelem1  26009  dvcnvrelem2  26010  dvfsumle  26013  dvfsumabs  26015  dvfsumlem2  26019  itgsubstlem  26040  mdegleb  26054  mdeglt  26055  mdegldg  26056  mdegxrcl  26057  mdegcl  26059  ig1peu  26165  reeff1olem  26436  logccv  26652  rlimcnp2  26955  lgamgulmlem2  27018  ppisval  27092  prmdvdsfi  27095  mumul  27169  sqff1o  27170  chtlepsi  27194  chpub  27208  dchrisum0lem2a  27505  pntlem3  27597  nosupno  27692  noetalem1  27730  cutlt  27949  negsproplem2  28046  onsbnd  28298  ex-res  30536  htthlem  31013  chlejb1i  31572  ssmd2  32408  fz2ssnn0  32884  gsumpart  33151  gsumhashmul  33155  elrgspnsubrunlem2  33336  extvfvcl  33727  mplvrpmrhm  33738  esplyind  33766  vietalem  33770  locfinreflem  34031  sibfof  34531  sitgclbn  34534  sitgaddlemb  34539  eulerpartlemgu  34568  ballotlemsima  34707  reprinrn  34809  bnj1311  35213  fnrelpredd  35279  erdsze2lem2  35439  iccllysconn  35485  cvmopnlem  35513  msrf  35777  neiin  36567  neibastop1  36594  neibastop2lem  36595  topmeet  36599  ttciunun  36746  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem19  38013  poimirlem30  38024  cnambfre  38042  itg2gt0cn  38049  sstotbnd2  38148  sstotbnd3  38150  ssbnd  38162  ismtyima  38177  heibor1lem  38183  idresssidinxp  38688  pmodlem2  40346  pmodN  40349  diaintclN  41557  djaclN  41635  dibintclN  41666  dicval  41675  dihoml4c  41875  djhcl  41899  infdesc  43100  isnacs2  43162  isnacs3  43166  diophrw  43215  pellfundre  43333  pellfundge  43334  pellfundlb  43336  pellfundglb  43337  fnwe2lem2  43503  lmhmfgima  43536  hbt  43582  omabs2  43784  nadd2rabord  43837  nadd1rabord  43841  cnvtrcl0  44077  trclrelexplem  44162  relexp0a  44167  isotone2  44500  imo72b2lem1  44620  tcfr  45414  modelaxreplem1  45429  wfac8prim  45453  climinf  46058  islptre  46071  limccog  46072  limcleqr  46094  limsupvaluz2  46188  itgcoscmulx  46419  ismbl3  46436  ismbl4  46443  stoweidlem27  46477  dirkercncflem2  46554  fourierdlem38  46595  fourierdlem49  46605  fourierdlem51  46607  fourierdlem54  46610  fourierdlem63  46619  fourierdlem68  46624  fourierdlem69  46625  fourierdlem70  46626  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem80  46636  fourierdlem84  46640  fourierdlem85  46641  fourierdlem88  46644  fourierdlem100  46656  fourierdlem101  46657  fourierdlem104  46660  fourierdlem107  46663  fourierdlem111  46667  fourierdlem112  46668  caragenel2d  46982  hoidmv1lelem3  47043  hspmbllem3  47078  sssmf  47188  smfrec  47239  smfsuplem1  47261