Theorem sstrid 3958

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

Syntax hints:   → wi 4   ⊆ wss 3914

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 3931

This theorem is referenced by:  difsymssdifssd  4227  wereu2  5635  sofld  6160  resssxp  6243  frpomin  6313  fimass  6708  fvmptss  6980  isofr2  7319  frxp  8105  fnse  8112  frxp2  8123  frxp3  8130  frrlem4  8268  frrlem13  8277  fprlem1  8279  smores2  8323  naddunif  8657  dffi3  9382  marypha1lem  9384  ordtypelem7  9477  ordtypelem8  9478  oismo  9493  unxpwdom2  9541  cantnfres  9630  oemapvali  9637  frmin  9702  frrlem15  9710  frrlem16  9711  tskwe  9903  acndom2  10007  dfac2a  10083  dfac12lem2  10098  cfle  10207  cofsmo  10222  coftr  10226  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  enfin1ai  10337  fin1a2lem12  10364  ttukeylem7  10468  alephexp1  10532  fpwwe2lem12  10595  fpwwe2  10596  canth4  10600  canthwelem  10603  pwfseqlem1  10611  pwfseqlem4  10615  fzossnn0  13651  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  xptrrel  14946  limsupgle  15443  limsupgre  15447  rlimres  15524  lo1res  15525  lo1resb  15530  rlimresb  15531  o1resb  15532  o1of2  15579  o1rlimmul  15585  isercolllem2  15632  isercoll  15634  climsup  15636  fprodntriv  15908  bitsinvp1  16419  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadasslem  16440  sadeq  16442  bitsres  16443  smuval2  16452  smupval  16458  smueqlem  16460  smumul  16463  1arith  16898  isstruct2  17119  setscom  17150  ressress  17217  imasvscafn  17500  imasless  17503  mrcssv  17575  isacs1i  17618  mreacs  17619  acsfn  17620  isacs4lem  18503  isacs5lem  18504  mgmhmima  18642  mhmima  18752  cntzmhm  19273  f1omvdconj  19376  f1omvdco2  19378  symgsssg  19397  symggen  19400  efgval  19647  gsumzaddlem  19851  gsumconst  19864  dmdprdd  19931  dprdfeq0  19954  dprdres  19960  dprdss  19961  dprdz  19962  subgdmdprd  19966  dprddisj2  19971  dprd2dlem1  19973  dprd2da  19974  dprd2d2  19976  dmdprdsplit2lem  19977  lmhmlsp  20956  lsppratlem4  21060  islbs3  21065  lbsextlem3  21070  znleval  21464  evpmss  21495  frlmsslsp  21705  lindff1  21729  lindfrn  21730  f1lindf  21731  lindfmm  21736  lsslindf  21739  mplcoe5  21947  mplind  21977  basdif0  22840  tgcl  22856  ppttop  22894  epttop  22896  ntrin  22948  mretopd  22979  neiptoptop  23018  cnclsi  23159  cnconst2  23170  cnrest2  23173  cnpresti  23175  cnprest2  23177  fiuncmp  23291  connsub  23308  connima  23312  iunconnlem  23314  1stcfb  23332  2ndc1stc  23338  2ndcdisj  23343  kgentopon  23425  llycmpkgen2  23437  1stckgenlem  23440  kgencn3  23445  ptclsg  23502  ptcnplem  23508  txtube  23527  hausdiag  23532  txkgen  23539  xkoco1cn  23544  xkoco2cn  23545  xkococnlem  23546  qtoptop2  23586  basqtop  23598  imastopn  23607  hmeores  23658  hmphdis  23683  ptcmpfi  23700  fbssfi  23724  filin  23741  infil  23750  fgtr  23777  elfm  23834  hausflim  23868  flimclslem  23871  fclscmp  23917  cnextcn  23954  tmdgsum2  23983  tgpconncomp  24000  ustexsym  24103  ustund  24109  ustimasn  24116  utoptop  24122  utopbas  24123  restutopopn  24126  blin2  24317  metustexhalf  24444  icccmplem2  24712  icccmplem3  24713  reconnlem2  24716  tcphcph  25137  fmcfil  25172  resscdrg  25258  ivthlem2  25353  ivthlem3  25354  ivth2  25356  ovolfiniun  25402  ovoliunlem1  25403  ismbl2  25428  nulmbl2  25437  unmbl  25438  shftmbl  25439  voliunlem1  25451  voliunlem2  25452  ioombl1lem4  25462  uniioombllem4  25487  uniioombllem5  25488  dyadmbllem  25500  dyadmbl  25501  mbflimsup  25567  i1fima  25579  i1fima2  25580  i1fadd  25596  itg1addlem4  25600  itg2splitlem  25649  itg2split  25650  ellimc3  25780  limcflflem  25781  limcflf  25782  limcresi  25786  limciun  25795  dvreslem  25810  dvres2lem  25811  dvres  25812  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvlip  25898  dvlip2  25900  c1liplem1  25901  dvivthlem1  25913  dvne0  25916  lhop1lem  25918  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  mdegleb  25969  mdeglt  25970  mdegldg  25971  mdegxrcl  25972  mdegcl  25974  ig1peu  26080  reeff1olem  26356  logccv  26572  rlimcnp2  26876  lgamgulmlem2  26940  ppisval  27014  prmdvdsfi  27017  mumul  27091  sqff1o  27092  chtlepsi  27117  chpub  27131  dchrisum0lem2a  27428  pntlem3  27520  nosupno  27615  noetalem1  27653  cutlt  27840  negsproplem2  27935  ex-res  30370  htthlem  30846  chlejb1i  31405  ssmd2  32241  fz2ssnn0  32708  gsumpart  32997  gsumhashmul  33001  gsumle  33038  elrgspnsubrunlem2  33199  locfinreflem  33830  sibfof  34331  sitgclbn  34334  sitgaddlemb  34339  eulerpartlemgu  34368  ballotlemsima  34507  reprinrn  34609  bnj1311  35014  fnrelpredd  35079  erdsze2lem2  35191  iccllysconn  35237  cvmopnlem  35265  msrf  35529  neiin  36320  neibastop1  36347  neibastop2lem  36348  topmeet  36352  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem19  37633  poimirlem30  37644  cnambfre  37662  itg2gt0cn  37669  sstotbnd2  37768  sstotbnd3  37770  ssbnd  37782  ismtyima  37797  heibor1lem  37803  idresssidinxp  38296  pmodlem2  39841  pmodN  39844  diaintclN  41052  djaclN  41130  dibintclN  41161  dicval  41170  dihoml4c  41370  djhcl  41394  infdesc  42631  isnacs2  42694  isnacs3  42698  diophrw  42747  pellfundre  42869  pellfundge  42870  pellfundlb  42872  pellfundglb  42873  fnwe2lem2  43040  lmhmfgima  43073  hbt  43119  omabs2  43321  nadd2rabord  43374  nadd1rabord  43378  cnvtrcl0  43615  trclrelexplem  43700  relexp0a  43705  isotone2  44038  imo72b2lem1  44158  tcfr  44953  modelaxreplem1  44968  wfac8prim  44992  climinf  45604  islptre  45617  limccog  45618  limcleqr  45642  limsupvaluz2  45736  itgcoscmulx  45967  ismbl3  45984  ismbl4  45991  stoweidlem27  46025  dirkercncflem2  46102  fourierdlem38  46143  fourierdlem49  46153  fourierdlem51  46155  fourierdlem54  46158  fourierdlem63  46167  fourierdlem68  46172  fourierdlem69  46173  fourierdlem70  46174  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem80  46184  fourierdlem84  46188  fourierdlem85  46189  fourierdlem88  46192  fourierdlem100  46204  fourierdlem101  46205  fourierdlem104  46208  fourierdlem107  46211  fourierdlem111  46215  fourierdlem112  46216  caragenel2d  46530  hoidmv1lelem3  46591  hspmbllem3  46626  sssmf  46736  smfrec  46787  smfsuplem1  46809