Theorem sstrid 3946

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

Syntax hints:   → wi 4   ⊆ wss 3902

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 3919

This theorem is referenced by:  difsymssdifssd  4214  wereu2  5613  sofld  6134  resssxp  6217  frpomin  6287  fimass  6671  fvmptss  6941  isofr2  7278  frxp  8056  fnse  8063  frxp2  8074  frxp3  8081  frrlem4  8219  frrlem13  8228  fprlem1  8230  smores2  8274  naddunif  8608  dffi3  9315  marypha1lem  9317  ordtypelem7  9410  ordtypelem8  9411  oismo  9426  unxpwdom2  9474  cantnfres  9567  oemapvali  9574  frmin  9642  frrlem15  9650  frrlem16  9651  tskwe  9843  acndom2  9945  dfac2a  10021  dfac12lem2  10036  cfle  10145  cofsmo  10160  coftr  10164  isf34lem5  10269  isf34lem7  10270  isf34lem6  10271  enfin1ai  10275  fin1a2lem12  10302  ttukeylem7  10406  alephexp1  10470  fpwwe2lem12  10533  fpwwe2  10534  canth4  10538  canthwelem  10541  pwfseqlem1  10549  pwfseqlem4  10553  fzossnn0  13590  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  xptrrel  14887  limsupgle  15384  limsupgre  15388  rlimres  15465  lo1res  15466  lo1resb  15471  rlimresb  15472  o1resb  15473  o1of2  15520  o1rlimmul  15526  isercolllem2  15573  isercoll  15575  climsup  15577  fprodntriv  15849  bitsinvp1  16360  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadasslem  16381  sadeq  16383  bitsres  16384  smuval2  16393  smupval  16399  smueqlem  16401  smumul  16404  1arith  16839  isstruct2  17060  setscom  17091  ressress  17158  imasvscafn  17441  imasless  17444  mrcssv  17520  isacs1i  17563  mreacs  17564  acsfn  17565  isacs4lem  18450  isacs5lem  18451  mgmhmima  18623  mhmima  18733  cntzmhm  19254  f1omvdconj  19359  f1omvdco2  19361  symgsssg  19380  symggen  19383  efgval  19630  gsumzaddlem  19834  gsumconst  19847  dmdprdd  19914  dprdfeq0  19937  dprdres  19943  dprdss  19944  dprdz  19945  subgdmdprd  19949  dprddisj2  19954  dprd2dlem1  19956  dprd2da  19957  dprd2d2  19959  dmdprdsplit2lem  19960  gsumle  20058  lmhmlsp  20984  lsppratlem4  21088  islbs3  21093  lbsextlem3  21098  znleval  21492  evpmss  21524  frlmsslsp  21734  lindff1  21758  lindfrn  21759  f1lindf  21760  lindfmm  21765  lsslindf  21768  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  30419  htthlem  30895  chlejb1i  31454  ssmd2  32290  fz2ssnn0  32766  gsumpart  33035  gsumhashmul  33039  elrgspnsubrunlem2  33213  mplvrpmrhm  33575  locfinreflem  33851  sibfof  34351  sitgclbn  34354  sitgaddlemb  34359  eulerpartlemgu  34388  ballotlemsima  34527  reprinrn  34629  bnj1311  35034  fnrelpredd  35100  erdsze2lem2  35246  iccllysconn  35292  cvmopnlem  35320  msrf  35584  neiin  36372  neibastop1  36399  neibastop2lem  36400  topmeet  36404  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem11  37677  poimirlem12  37678  poimirlem16  37682  poimirlem19  37685  poimirlem30  37696  cnambfre  37714  itg2gt0cn  37721  sstotbnd2  37820  sstotbnd3  37822  ssbnd  37834  ismtyima  37849  heibor1lem  37855  idresssidinxp  38348  pmodlem2  39892  pmodN  39895  diaintclN  41103  djaclN  41181  dibintclN  41212  dicval  41221  dihoml4c  41421  djhcl  41445  infdesc  42682  isnacs2  42745  isnacs3  42749  diophrw  42798  pellfundre  42920  pellfundge  42921  pellfundlb  42923  pellfundglb  42924  fnwe2lem2  43090  lmhmfgima  43123  hbt  43169  omabs2  43371  nadd2rabord  43424  nadd1rabord  43428  cnvtrcl0  43665  trclrelexplem  43750  relexp0a  43755  isotone2  44088  imo72b2lem1  44208  tcfr  45002  modelaxreplem1  45017  wfac8prim  45041  climinf  45652  islptre  45665  limccog  45666  limcleqr  45688  limsupvaluz2  45782  itgcoscmulx  46013  ismbl3  46030  ismbl4  46037  stoweidlem27  46071  dirkercncflem2  46148  fourierdlem38  46189  fourierdlem49  46199  fourierdlem51  46201  fourierdlem54  46204  fourierdlem63  46213  fourierdlem68  46218  fourierdlem69  46219  fourierdlem70  46220  fourierdlem74  46224  fourierdlem75  46225  fourierdlem76  46226  fourierdlem80  46230  fourierdlem84  46234  fourierdlem85  46235  fourierdlem88  46238  fourierdlem100  46250  fourierdlem101  46251  fourierdlem104  46254  fourierdlem107  46257  fourierdlem111  46261  fourierdlem112  46262  caragenel2d  46576  hoidmv1lelem3  46637  hspmbllem3  46672  sssmf  46782  smfrec  46833  smfsuplem1  46855