Theorem sstrid 3995

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

Syntax hints:   → wi 4   ⊆ wss 3951

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3968

This theorem is referenced by:  difsymssdifssd  4264  wereu2  5682  sofld  6207  resssxp  6290  frpomin  6361  fimass  6756  fvmptss  7028  isofr2  7364  frxp  8151  fnse  8158  frxp2  8169  frxp3  8176  frrlem4  8314  frrlem13  8323  fprlem1  8325  smores2  8394  naddunif  8731  dffi3  9471  marypha1lem  9473  ordtypelem7  9564  ordtypelem8  9565  oismo  9580  unxpwdom2  9628  cantnfres  9717  oemapvali  9724  frmin  9789  frrlem15  9797  frrlem16  9798  tskwe  9990  acndom2  10094  dfac2a  10170  dfac12lem2  10185  cfle  10294  cofsmo  10309  coftr  10313  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  enfin1ai  10424  fin1a2lem12  10451  ttukeylem7  10555  alephexp1  10619  fpwwe2lem12  10682  fpwwe2  10683  canth4  10687  canthwelem  10690  pwfseqlem1  10698  pwfseqlem4  10702  fzossnn0  13730  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  xptrrel  15019  limsupgle  15513  limsupgre  15517  rlimres  15594  lo1res  15595  lo1resb  15600  rlimresb  15601  o1resb  15602  o1of2  15649  o1rlimmul  15655  isercolllem2  15702  isercoll  15704  climsup  15706  fprodntriv  15978  bitsinvp1  16486  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadasslem  16507  sadeq  16509  bitsres  16510  smuval2  16519  smupval  16525  smueqlem  16527  smumul  16530  1arith  16965  isstruct2  17186  setscom  17217  ressress  17293  imasvscafn  17582  imasless  17585  mrcssv  17657  isacs1i  17700  mreacs  17701  acsfn  17702  isacs4lem  18589  isacs5lem  18590  mgmhmima  18728  mhmima  18838  cntzmhm  19359  f1omvdconj  19464  f1omvdco2  19466  symgsssg  19485  symggen  19488  efgval  19735  gsumzaddlem  19939  gsumconst  19952  dmdprdd  20019  dprdfeq0  20042  dprdres  20048  dprdss  20049  dprdz  20050  subgdmdprd  20054  dprddisj2  20059  dprd2dlem1  20061  dprd2da  20062  dprd2d2  20064  dmdprdsplit2lem  20065  lmhmlsp  21048  lsppratlem4  21152  islbs3  21157  lbsextlem3  21162  znleval  21573  evpmss  21604  frlmsslsp  21816  lindff1  21840  lindfrn  21841  f1lindf  21842  lindfmm  21847  lsslindf  21850  mplcoe5  22058  mplind  22094  basdif0  22960  tgcl  22976  ppttop  23014  epttop  23016  ntrin  23069  mretopd  23100  neiptoptop  23139  cnclsi  23280  cnconst2  23291  cnrest2  23294  cnpresti  23296  cnprest2  23298  fiuncmp  23412  connsub  23429  connima  23433  iunconnlem  23435  1stcfb  23453  2ndc1stc  23459  2ndcdisj  23464  kgentopon  23546  llycmpkgen2  23558  1stckgenlem  23561  kgencn3  23566  ptclsg  23623  ptcnplem  23629  txtube  23648  hausdiag  23653  txkgen  23660  xkoco1cn  23665  xkoco2cn  23666  xkococnlem  23667  qtoptop2  23707  basqtop  23719  imastopn  23728  hmeores  23779  hmphdis  23804  ptcmpfi  23821  fbssfi  23845  filin  23862  infil  23871  fgtr  23898  elfm  23955  hausflim  23989  flimclslem  23992  fclscmp  24038  cnextcn  24075  tmdgsum2  24104  tgpconncomp  24121  ustexsym  24224  ustund  24230  ustimasn  24237  utoptop  24243  utopbas  24244  restutopopn  24247  blin2  24439  metustexhalf  24569  icccmplem2  24845  icccmplem3  24846  reconnlem2  24849  tcphcph  25271  fmcfil  25306  resscdrg  25392  ivthlem2  25487  ivthlem3  25488  ivth2  25490  ovolfiniun  25536  ovoliunlem1  25537  ismbl2  25562  nulmbl2  25571  unmbl  25572  shftmbl  25573  voliunlem1  25585  voliunlem2  25586  ioombl1lem4  25596  uniioombllem4  25621  uniioombllem5  25622  dyadmbllem  25634  dyadmbl  25635  mbflimsup  25701  i1fima  25713  i1fima2  25714  i1fadd  25730  itg1addlem4  25734  itg2splitlem  25783  itg2split  25784  ellimc3  25914  limcflflem  25915  limcflf  25916  limcresi  25920  limciun  25929  dvreslem  25944  dvres2lem  25945  dvres  25946  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvlip  26032  dvlip2  26034  c1liplem1  26035  dvivthlem1  26047  dvne0  26050  lhop1lem  26052  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubstlem  26089  mdegleb  26103  mdeglt  26104  mdegldg  26105  mdegxrcl  26106  mdegcl  26108  ig1peu  26214  reeff1olem  26490  logccv  26705  rlimcnp2  27009  lgamgulmlem2  27073  ppisval  27147  prmdvdsfi  27150  mumul  27224  sqff1o  27225  chtlepsi  27250  chpub  27264  dchrisum0lem2a  27561  pntlem3  27653  nosupno  27748  noetalem1  27786  cutlt  27966  negsproplem2  28061  ex-res  30460  htthlem  30936  chlejb1i  31495  ssmd2  32331  fz2ssnn0  32787  gsumpart  33060  gsumhashmul  33064  gsumle  33101  elrgspnsubrunlem2  33252  locfinreflem  33839  sibfof  34342  sitgclbn  34345  sitgaddlemb  34350  eulerpartlemgu  34379  ballotlemsima  34518  reprinrn  34633  bnj1311  35038  fnrelpredd  35103  erdsze2lem2  35209  iccllysconn  35255  cvmopnlem  35283  msrf  35547  neiin  36333  neibastop1  36360  neibastop2lem  36361  topmeet  36365  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem19  37646  poimirlem30  37657  cnambfre  37675  itg2gt0cn  37682  sstotbnd2  37781  sstotbnd3  37783  ssbnd  37795  ismtyima  37810  heibor1lem  37816  idresssidinxp  38309  pmodlem2  39849  pmodN  39852  diaintclN  41060  djaclN  41138  dibintclN  41169  dicval  41178  dihoml4c  41378  djhcl  41402  infdesc  42653  isnacs2  42717  isnacs3  42721  diophrw  42770  pellfundre  42892  pellfundge  42893  pellfundlb  42895  pellfundglb  42896  fnwe2lem2  43063  lmhmfgima  43096  hbt  43142  omabs2  43345  nadd2rabord  43398  nadd1rabord  43402  cnvtrcl0  43639  trclrelexplem  43724  relexp0a  43729  isotone2  44062  imo72b2lem1  44182  tcfr  44980  modelaxreplem1  44995  wfac8prim  45019  climinf  45621  islptre  45634  limccog  45635  limcleqr  45659  limsupvaluz2  45753  itgcoscmulx  45984  ismbl3  46001  ismbl4  46008  stoweidlem27  46042  dirkercncflem2  46119  fourierdlem38  46160  fourierdlem49  46170  fourierdlem51  46172  fourierdlem54  46175  fourierdlem63  46184  fourierdlem68  46189  fourierdlem69  46190  fourierdlem70  46191  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem80  46201  fourierdlem84  46205  fourierdlem85  46206  fourierdlem88  46209  fourierdlem100  46221  fourierdlem101  46222  fourierdlem104  46225  fourierdlem107  46228  fourierdlem111  46232  fourierdlem112  46233  caragenel2d  46547  hoidmv1lelem3  46608  hspmbllem3  46643  sssmf  46753  smfrec  46804  smfsuplem1  46826