Theorem sstrid 3919

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

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

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

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

This theorem is used by:  difsymssdifssd  4209  wereu2  5647  sofld  6178  resssxp  6272  frpomin  6343  fimass  6730  fvmptss  7006  isofr2  7352  ovmptss  8104  frxp  8140  fnse  8152  frxp2  8163  frxp3  8170  frrlem4  8310  frrlem13  8319  fprlem1  8321  smores2  8365  naddunif  8706  dffi3  9426  marypha1lem  9428  ordtypelem7  9521  ordtypelem8  9522  oismo  9537  unxpwdom2  9585  cantnfres  9681  oemapvali  9688  frmin  9756  frrlem15  9764  frrlem16  9765  tskwe  10034  acndom2  10136  dfac2a  10211  dfac12lem2  10226  cfle  10334  cofsmo  10350  coftr  10354  isf34lem5  10459  isf34lem7  10460  isf34lem6  10461  enfin1ai  10465  fin1a2lem12  10492  ttukeylem7  10596  alephexp1  10667  fpwwe2lem12  10730  fpwwe2  10731  canth4  10735  canthwelem  10738  pwfseqlem1  10746  pwfseqlem4  10750  fzossnn0  13828  fsuppmapnn0fiublem  14136  fsuppmapnn0fiub  14137  xptrrel  15138  limsupgle  15649  limsupgre  15653  rlimres  15730  lo1res  15731  lo1resb  15736  rlimresb  15737  o1resb  15738  o1of2  15785  o1rlimmul  15791  isercolllem2  15838  isercoll  15840  climsup  15842  fprodntriv  16114  bitsinvp1  16624  sadcaddlem  16632  sadadd2lem  16634  sadadd3  16636  sadasslem  16645  sadeq  16647  bitsres  16648  smuval2  16657  smupval  16663  smueqlem  16665  smumul  16668  1arith  17110  isstruct2  17332  setscom  17363  ressress  17430  imasvscafn  17714  imasless  17717  mrcssv  17793  isacs1i  17836  mreacs  17837  acsfn  17838  isacs4lem  18723  isacs5lem  18724  mgmhmima  18909  mhmima  19026  cntzmhm  19560  f1omvdconj  19665  f1omvdco2  19667  symgsssg  19686  symggen  19689  efgval  19936  gsumzaddlem  20140  gsumconst  20153  dmdprdd  20220  dprdfeq0  20243  dprdres  20249  dprdss  20250  dprdz  20251  subgdmdprd  20255  dprddisj2  20260  dprd2dlem1  20262  dprd2da  20263  dprd2d2  20265  dmdprdsplit2lem  20266  gsumle  20364  lmhmlsp  21329  lsppratlem4  21433  islbs3  21438  lbsextlem3  21443  znleval  21865  evpmss  21897  frlmsslsp  22107  lindff1  22131  lindfrn  22132  f1lindf  22133  lindfmm  22138  lsslindf  22141  mplcoe5  22354  mplind  22384  basdif0  23276  tgcl  23292  ppttop  23330  epttop  23332  ntrin  23384  mretopd  23415  neiptoptop  23454  cnclsi  23595  cnconst2  23606  cnrest2  23609  cnpresti  23611  cnprest2  23613  fiuncmp  23727  connsub  23744  connima  23748  iunconnlem  23750  1stcfb  23768  2ndc1stc  23774  2ndcdisj  23780  kgentopon  23862  llycmpkgen2  23874  1stckgenlem  23877  kgencn3  23882  ptclsg  23939  ptcnplem  23945  txtube  23964  hausdiag  23969  txkgen  23976  xkoco1cn  23981  xkoco2cn  23982  xkococnlem  23983  qtoptop2  24023  basqtop  24035  imastopn  24044  hmeores  24095  hmphdis  24120  ptcmpfi  24137  fbssfi  24161  filin  24178  infil  24187  fgtr  24214  elfm  24271  hausflim  24305  flimclslem  24308  fclscmp  24354  cnextcn  24391  tmdgsum2  24420  tgpconncomp  24437  ustexsym  24540  ustund  24546  ustimasn  24552  utoptop  24558  utopbas  24559  restutopopn  24562  blin2  24753  metustexhalf  24880  icccmplem2  25148  icccmplem3  25149  reconnlem2  25152  tcphcph  25563  fmcfil  25598  resscdrg  25684  ivthlem2  25778  ivthlem3  25779  ivth2  25781  ovolfiniun  25827  ovoliunlem1  25828  ismbl2  25853  nulmbl2  25862  unmbl  25863  shftmbl  25864  voliunlem1  25876  voliunlem2  25877  ioombl1lem4  25887  uniioombllem4  25912  uniioombllem5  25913  dyadmbllem  25925  dyadmbl  25926  mbflimsup  25992  i1fima  26004  i1fima2  26005  i1fadd  26021  itg1addlem4  26025  itg2splitlem  26074  itg2split  26075  ellimc3  26204  limcflflem  26205  limcflf  26206  limcresi  26210  limciun  26219  dvreslem  26234  dvres2lem  26235  dvres  26236  dvaddbr  26263  dvmulbr  26264  dvlip  26318  dvlip2  26320  c1liplem1  26321  dvivthlem1  26333  dvne0  26336  lhop1lem  26338  lhop  26341  dvcnvrelem1  26342  dvcnvrelem2  26343  dvfsumle  26346  dvfsumabs  26348  dvfsumlem2  26352  itgsubstlem  26373  mdegleb  26387  mdeglt  26388  mdegldg  26389  mdegxrcl  26390  mdegcl  26392  ig1peu  26498  reeff1olem  26778  logccv  26996  rlimcnp2  27299  lgamgulmlem2  27362  ppisval  27436  prmdvdsfi  27439  mumul  27513  sqff1o  27514  chtlepsi  27538  chpub  27552  dchrisum0lem2a  27849  pntlem3  27941  infdesc  27972  nosupno  28065  noetalem1  28103  cutlt  28323  negsproplem2  28420  onsbnd  28672  cgrabasimass  29383  ex-res  31047  htthlem  31524  chlejb1i  32083  ssmd2  32919  fz2ssnn0  33423  gsumpart  33670  gsumhashmul  33674  elrgspnsubrunlem2  33855  extvfvcl  34214  mplvrpmrhm  34225  esplyind  34253  vietalem  34257  locfinreflem  34518  sibfof  35018  sitgclbn  35021  sitgaddlemb  35026  eulerpartlemgu  35055  ballotlemsima  35194  reprinrn  35293  bnj1311  35700  fnrelpredd  35772  erdsze2lem2  36055  iccllysconn  36101  cvmopnlem  36129  msrf  36393  neiin  37212  neibastop1  37239  neibastop2lem  37240  topmeet  37244  ttciunun  37391  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem11  38642  poimirlem12  38643  poimirlem16  38647  poimirlem19  38650  poimirlem30  38661  cnambfre  38679  itg2gt0cn  38686  sstotbnd2  38801  sstotbnd3  38803  ssbnd  38815  ismtyima  38830  heibor1lem  38836  idresssidinxp  39339  pmodlem2  40997  pmodN  41000  diaintclN  42208  djaclN  42286  dibintclN  42317  dicval  42326  dihoml4c  42526  djhcl  42550  isnacs2  43810  isnacs3  43814  diophrw  43863  pellfundre  43981  pellfundge  43982  pellfundlb  43984  pellfundglb  43985  lmhmfgima  44179  hbt  44225  omabs2  44427  nadd2rabord  44480  nadd1rabord  44484  cnvtrcl0  44719  trclrelexplem  44804  relexp0a  44809  isotone2  45142  imo72b2lem1  45262  tcfr  46046  modelaxreplem1  46061  wfac8prim  46085  climinf  46711  islptre  46724  limccog  46725  limcleqr  46747  limsupvaluz2  46841  itgcoscmulx  47072  ismbl3  47089  ismbl4  47096  stoweidlem27  47130  dirkercncflem2  47207  fourierdlem38  47248  fourierdlem51  47260  fourierdlem54  47263  fourierdlem63  47272  fourierdlem68  47277  fourierdlem69  47278  fourierdlem70  47279  fourierdlem74  47283  fourierdlem75  47284  fourierdlem76  47285  fourierdlem80  47289  fourierdlem84  47293  fourierdlem85  47294  fourierdlem88  47297  fourierdlem100  47309  fourierdlem101  47310  fourierdlem104  47313  fourierdlem107  47316  fourierdlem111  47320  fourierdlem112  47321  caragenel2d  47635  hoidmv1lelem3  47696  hspmbllem3  47731  sssmf  47841  smfrec  47892  smfsuplem1  47914