Theorem sstrid 3993

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

Syntax hints:   → wi 4   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  difsymssdifssd  4253  wereu2  5673  sofld  6186  resssxp  6269  frpomin  6341  fimass  6738  fvmptss  7010  fimacnvOLD  7072  isofr2  7344  frxp  8117  fnse  8124  frxp2  8135  frxp3  8142  frrlem4  8280  frrlem13  8289  fprlem1  8291  smores2  8360  naddunif  8698  dffi3  9432  marypha1lem  9434  ordtypelem7  9525  ordtypelem8  9526  oismo  9541  unxpwdom2  9589  cantnfres  9678  oemapvali  9685  frmin  9750  frrlem15  9758  frrlem16  9759  tskwe  9951  acndom2  10055  dfac2a  10130  dfac12lem2  10145  cfle  10255  cofsmo  10270  coftr  10274  isf34lem5  10379  isf34lem7  10380  isf34lem6  10381  enfin1ai  10385  fin1a2lem12  10412  ttukeylem7  10516  alephexp1  10580  fpwwe2lem12  10643  fpwwe2  10644  canth4  10648  canthwelem  10651  pwfseqlem1  10659  pwfseqlem4  10663  fzossnn0  13670  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  xptrrel  14934  limsupgle  15428  limsupgre  15432  rlimres  15509  lo1res  15510  lo1resb  15515  rlimresb  15516  o1resb  15517  o1of2  15564  o1rlimmul  15570  isercolllem2  15619  isercoll  15621  climsup  15623  fprodntriv  15893  bitsinvp1  16397  sadcaddlem  16405  sadadd2lem  16407  sadadd3  16409  sadasslem  16418  sadeq  16420  bitsres  16421  smuval2  16430  smupval  16436  smueqlem  16438  smumul  16441  1arith  16867  isstruct2  17089  setscom  17120  ressress  17200  imasvscafn  17490  imasless  17493  mrcssv  17565  isacs1i  17608  mreacs  17609  acsfn  17610  isacs4lem  18507  isacs5lem  18508  mgmhmima  18646  mhmima  18748  cntzmhm  19253  f1omvdconj  19362  f1omvdco2  19364  symgsssg  19383  symggen  19386  efgval  19633  gsumzaddlem  19837  gsumconst  19850  dmdprdd  19917  dprdfeq0  19940  dprdres  19946  dprdss  19947  dprdz  19948  subgdmdprd  19952  dprddisj2  19957  dprd2dlem1  19959  dprd2da  19960  dprd2d2  19962  dmdprdsplit2lem  19963  lmhmlsp  20893  lsppratlem4  20997  islbs3  21002  lbsextlem3  21007  znleval  21420  evpmss  21449  frlmsslsp  21661  lindff1  21685  lindfrn  21686  f1lindf  21687  lindfmm  21692  lsslindf  21695  mplcoe5  21906  mplind  21942  basdif0  22776  tgcl  22792  ppttop  22830  epttop  22832  ntrin  22885  mretopd  22916  neiptoptop  22955  cnclsi  23096  cnconst2  23107  cnrest2  23110  cnpresti  23112  cnprest2  23114  fiuncmp  23228  connsub  23245  connima  23249  iunconnlem  23251  1stcfb  23269  2ndc1stc  23275  2ndcdisj  23280  kgentopon  23362  llycmpkgen2  23374  1stckgenlem  23377  kgencn3  23382  ptclsg  23439  ptcnplem  23445  txtube  23464  hausdiag  23469  txkgen  23476  xkoco1cn  23481  xkoco2cn  23482  xkococnlem  23483  qtoptop2  23523  basqtop  23535  imastopn  23544  hmeores  23595  hmphdis  23620  ptcmpfi  23637  fbssfi  23661  filin  23678  infil  23687  fgtr  23714  elfm  23771  hausflim  23805  flimclslem  23808  fclscmp  23854  cnextcn  23891  tmdgsum2  23920  tgpconncomp  23937  ustexsym  24040  ustund  24046  ustimasn  24053  utoptop  24059  utopbas  24060  restutopopn  24063  blin2  24255  metustexhalf  24385  icccmplem2  24659  icccmplem3  24660  reconnlem2  24663  tcphcph  25085  fmcfil  25120  resscdrg  25206  ivthlem2  25301  ivthlem3  25302  ivth2  25304  ovolfiniun  25350  ovoliunlem1  25351  ismbl2  25376  nulmbl2  25385  unmbl  25386  shftmbl  25387  voliunlem1  25399  voliunlem2  25400  ioombl1lem4  25410  uniioombllem4  25435  uniioombllem5  25436  dyadmbllem  25448  dyadmbl  25449  mbflimsup  25515  i1fima  25527  i1fima2  25528  i1fadd  25544  itg1addlem4  25548  itg1addlem4OLD  25549  itg2splitlem  25598  itg2split  25599  ellimc3  25728  limcflflem  25729  limcflf  25730  limcresi  25734  limciun  25743  dvreslem  25758  dvres2lem  25759  dvres  25760  dvaddbr  25788  dvmulbr  25789  dvmulbrOLD  25790  dvlip  25846  dvlip2  25848  c1liplem1  25849  dvivthlem1  25861  dvne0  25864  lhop1lem  25866  lhop  25869  dvcnvrelem1  25870  dvcnvrelem2  25871  dvfsumle  25874  dvfsumleOLD  25875  dvfsumabs  25877  dvfsumlem2  25881  dvfsumlem2OLD  25882  itgsubstlem  25903  mdegleb  25920  mdeglt  25921  mdegldg  25922  mdegxrcl  25923  mdegcl  25925  ig1peu  26027  reeff1olem  26298  logccv  26511  rlimcnp2  26812  lgamgulmlem2  26875  ppisval  26949  prmdvdsfi  26952  mumul  27026  sqff1o  27027  chtlepsi  27052  chpub  27066  dchrisum0lem2a  27363  pntlem3  27455  nosupno  27549  noetalem1  27587  cutlt  27765  negsproplem2  27854  ex-res  30127  htthlem  30603  chlejb1i  31162  ssmd2  31998  fz2ssnn0  32429  gsumpart  32643  gsumhashmul  32644  gsumle  32678  locfinreflem  33284  sibfof  33803  sitgclbn  33806  sitgaddlemb  33811  eulerpartlemgu  33840  ballotlemsima  33978  reprinrn  34094  bnj1311  34499  fnrelpredd  34556  erdsze2lem2  34659  iccllysconn  34705  cvmopnlem  34733  msrf  34997  neiin  35681  neibastop1  35708  neibastop2lem  35709  topmeet  35713  poimirlem1  36953  poimirlem2  36954  poimirlem3  36955  poimirlem11  36963  poimirlem12  36964  poimirlem16  36968  poimirlem19  36971  poimirlem30  36982  cnambfre  37000  itg2gt0cn  37007  sstotbnd2  37106  sstotbnd3  37108  ssbnd  37120  ismtyima  37135  heibor1lem  37141  idresssidinxp  37641  pmodlem2  39182  pmodN  39185  diaintclN  40393  djaclN  40471  dibintclN  40502  dicval  40511  dihoml4c  40711  djhcl  40735  infdesc  41848  isnacs2  41907  isnacs3  41911  diophrw  41960  pellfundre  42082  pellfundge  42083  pellfundlb  42085  pellfundglb  42086  fnwe2lem2  42256  lmhmfgima  42289  hbt  42335  omabs2  42545  nadd2rabord  42598  nadd1rabord  42602  cnvtrcl0  42840  trclrelexplem  42925  relexp0a  42930  isotone2  43263  imo72b2lem1  43384  climinf  44781  islptre  44794  limccog  44795  limcleqr  44819  itgcoscmulx  45144  ismbl3  45161  ismbl4  45168  stoweidlem27  45202  dirkercncflem2  45279  fourierdlem38  45320  fourierdlem49  45330  fourierdlem51  45332  fourierdlem54  45335  fourierdlem63  45344  fourierdlem68  45349  fourierdlem69  45350  fourierdlem70  45351  fourierdlem74  45355  fourierdlem75  45356  fourierdlem76  45357  fourierdlem80  45361  fourierdlem84  45365  fourierdlem85  45366  fourierdlem88  45369  fourierdlem100  45381  fourierdlem101  45382  fourierdlem104  45385  fourierdlem107  45388  fourierdlem111  45392  fourierdlem112  45393  caragenel2d  45707  hoidmv1lelem3  45768  hspmbllem3  45803  sssmf  45913  smfrec  45964  smfsuplem1  45986