Theorem sstrid 3945

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3919

This theorem is used by:  difsymssdifssd  4213  wereu2  5656  sofld  6184  resssxp  6271  frpomin  6342  fimass  6727  fvmptss  7003  isofr2  7349  frxp  8128  fnse  8135  frxp2  8146  frxp3  8153  frrlem4  8292  frrlem13  8301  fprlem1  8303  smores2  8347  naddunif  8686  dffi3  9405  marypha1lem  9407  ordtypelem7  9500  ordtypelem8  9501  oismo  9516  unxpwdom2  9564  cantnfres  9660  oemapvali  9667  frmin  9735  frrlem15  9743  frrlem16  9744  tskwe  9959  acndom2  10061  dfac2a  10136  dfac12lem2  10151  cfle  10259  cofsmo  10275  coftr  10279  isf34lem5  10384  isf34lem7  10385  isf34lem6  10386  enfin1ai  10390  fin1a2lem12  10417  ttukeylem7  10521  alephexp1  10592  fpwwe2lem12  10655  fpwwe2  10656  canth4  10660  canthwelem  10663  pwfseqlem1  10671  pwfseqlem4  10675  fzossnn0  13750  fsuppmapnn0fiublem  14058  fsuppmapnn0fiub  14059  xptrrel  15057  limsupgle  15568  limsupgre  15572  rlimres  15649  lo1res  15650  lo1resb  15655  rlimresb  15656  o1resb  15657  o1of2  15704  o1rlimmul  15710  isercolllem2  15757  isercoll  15759  climsup  15761  fprodntriv  16035  bitsinvp1  16545  sadcaddlem  16553  sadadd2lem  16555  sadadd3  16557  sadasslem  16566  sadeq  16568  bitsres  16569  smuval2  16578  smupval  16584  smueqlem  16586  smumul  16589  1arith  17025  isstruct2  17247  setscom  17278  ressress  17345  imasvscafn  17629  imasless  17632  mrcssv  17708  isacs1i  17751  mreacs  17752  acsfn  17753  isacs4lem  18638  isacs5lem  18639  mgmhmima  18823  mhmima  18940  cntzmhm  19474  f1omvdconj  19579  f1omvdco2  19581  symgsssg  19600  symggen  19603  efgval  19850  gsumzaddlem  20054  gsumconst  20067  dmdprdd  20134  dprdfeq0  20157  dprdres  20163  dprdss  20164  dprdz  20165  subgdmdprd  20169  dprddisj2  20174  dprd2dlem1  20176  dprd2da  20177  dprd2d2  20179  dmdprdsplit2lem  20180  gsumle  20278  lmhmlsp  21239  lsppratlem4  21343  islbs3  21348  lbsextlem3  21353  znleval  21773  evpmss  21805  frlmsslsp  22015  lindff1  22039  lindfrn  22040  f1lindf  22041  lindfmm  22046  lsslindf  22049  mplcoe5  22262  mplind  22292  basdif0  23184  tgcl  23200  ppttop  23238  epttop  23240  ntrin  23292  mretopd  23323  neiptoptop  23362  cnclsi  23503  cnconst2  23514  cnrest2  23517  cnpresti  23519  cnprest2  23521  fiuncmp  23635  connsub  23652  connima  23656  iunconnlem  23658  1stcfb  23676  2ndc1stc  23682  2ndcdisj  23688  kgentopon  23770  llycmpkgen2  23782  1stckgenlem  23785  kgencn3  23790  ptclsg  23847  ptcnplem  23853  txtube  23872  hausdiag  23877  txkgen  23884  xkoco1cn  23889  xkoco2cn  23890  xkococnlem  23891  qtoptop2  23931  basqtop  23943  imastopn  23952  hmeores  24003  hmphdis  24028  ptcmpfi  24045  fbssfi  24069  filin  24086  infil  24095  fgtr  24122  elfm  24179  hausflim  24213  flimclslem  24216  fclscmp  24262  cnextcn  24299  tmdgsum2  24328  tgpconncomp  24345  ustexsym  24448  ustund  24454  ustimasn  24460  utoptop  24466  utopbas  24467  restutopopn  24470  blin2  24661  metustexhalf  24788  icccmplem2  25056  icccmplem3  25057  reconnlem2  25060  tcphcph  25471  fmcfil  25506  resscdrg  25592  ivthlem2  25686  ivthlem3  25687  ivth2  25689  ovolfiniun  25735  ovoliunlem1  25736  ismbl2  25761  nulmbl2  25770  unmbl  25771  shftmbl  25772  voliunlem1  25784  voliunlem2  25785  ioombl1lem4  25795  uniioombllem4  25820  uniioombllem5  25821  dyadmbllem  25833  dyadmbl  25834  mbflimsup  25900  i1fima  25912  i1fima2  25913  i1fadd  25929  itg1addlem4  25933  itg2splitlem  25982  itg2split  25983  ellimc3  26113  limcflflem  26114  limcflf  26115  limcresi  26119  limciun  26128  dvreslem  26143  dvres2lem  26144  dvres  26145  dvaddbr  26172  dvmulbr  26173  dvlip  26227  dvlip2  26229  c1liplem1  26230  dvivthlem1  26242  dvne0  26245  lhop1lem  26247  lhop  26250  dvcnvrelem1  26251  dvcnvrelem2  26252  dvfsumle  26255  dvfsumabs  26257  dvfsumlem2  26261  itgsubstlem  26282  mdegleb  26296  mdeglt  26297  mdegldg  26298  mdegxrcl  26299  mdegcl  26301  ig1peu  26407  reeff1olem  26689  logccv  26908  rlimcnp2  27211  lgamgulmlem2  27274  ppisval  27348  prmdvdsfi  27351  mumul  27425  sqff1o  27426  chtlepsi  27450  chpub  27464  dchrisum0lem2a  27761  pntlem3  27853  nosupno  27947  noetalem1  27985  cutlt  28205  negsproplem2  28302  onsbnd  28554  cgrabasimass  29265  ex-res  30929  htthlem  31406  chlejb1i  31965  ssmd2  32801  fz2ssnn0  33264  gsumpart  33511  gsumhashmul  33515  elrgspnsubrunlem2  33696  extvfvcl  34054  mplvrpmrhm  34065  esplyind  34093  vietalem  34097  locfinreflem  34358  sibfof  34859  sitgclbn  34862  sitgaddlemb  34867  eulerpartlemgu  34896  ballotlemsima  35035  reprinrn  35134  bnj1311  35541  fnrelpredd  35604  erdsze2lem2  35791  iccllysconn  35837  cvmopnlem  35865  msrf  36129  neiin  36959  neibastop1  36986  neibastop2lem  36987  topmeet  36991  ttciunun  37138  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem11  38388  poimirlem12  38389  poimirlem16  38393  poimirlem19  38396  poimirlem30  38407  cnambfre  38425  itg2gt0cn  38432  sstotbnd2  38532  sstotbnd3  38534  ssbnd  38546  ismtyima  38561  heibor1lem  38567  idresssidinxp  39070  pmodlem2  40728  pmodN  40731  diaintclN  41939  djaclN  42017  dibintclN  42048  dicval  42057  dihoml4c  42257  djhcl  42281  infdesc  43497  isnacs2  43559  isnacs3  43563  diophrw  43612  pellfundre  43730  pellfundge  43731  pellfundlb  43733  pellfundglb  43734  fnwe2lem2  43900  lmhmfgima  43933  hbt  43979  omabs2  44181  nadd2rabord  44234  nadd1rabord  44238  cnvtrcl0  44474  trclrelexplem  44559  relexp0a  44564  isotone2  44897  imo72b2lem1  45017  tcfr  45794  modelaxreplem1  45809  wfac8prim  45833  climinf  46444  islptre  46457  limccog  46458  limcleqr  46480  limsupvaluz2  46574  itgcoscmulx  46805  ismbl3  46822  ismbl4  46829  stoweidlem27  46863  dirkercncflem2  46940  fourierdlem38  46981  fourierdlem51  46993  fourierdlem54  46996  fourierdlem63  47005  fourierdlem68  47010  fourierdlem69  47011  fourierdlem70  47012  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem80  47022  fourierdlem84  47026  fourierdlem85  47027  fourierdlem88  47030  fourierdlem100  47042  fourierdlem101  47043  fourierdlem104  47046  fourierdlem107  47049  fourierdlem111  47053  fourierdlem112  47054  caragenel2d  47368  hoidmv1lelem3  47429  hspmbllem3  47464  sssmf  47574  smfrec  47625  smfsuplem1  47647