Theorem sstrid 3978

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

Syntax hints:   → wi 4   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  difsymssdifssd  4230  wereu2  5552  sofld  6044  fimass  6555  fvmptss  6780  fimacnv  6839  isofr2  7097  frxp  7820  fnse  7827  smores2  7991  dffi3  8895  marypha1lem  8897  ordtypelem7  8988  ordtypelem8  8989  oismo  9004  unxpwdom2  9052  cantnfres  9140  oemapvali  9147  tskwe  9379  acndom2  9480  dfac2a  9555  dfac12lem2  9570  cfle  9676  cofsmo  9691  coftr  9695  isf34lem5  9800  isf34lem7  9801  isf34lem6  9802  enfin1ai  9806  fin1a2lem12  9833  ttukeylem7  9937  alephexp1  10001  fpwwe2lem13  10064  fpwwe2  10065  canth4  10069  canthwelem  10072  pwfseqlem1  10080  pwfseqlem4  10084  fzossnn0  13069  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  xptrrel  14340  limsupgle  14834  limsupgre  14838  rlimres  14915  lo1res  14916  lo1resb  14921  rlimresb  14922  o1resb  14923  o1of2  14969  o1rlimmul  14975  isercolllem2  15022  isercoll  15024  climsup  15026  fprodntriv  15296  bitsinvp1  15798  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadasslem  15819  sadeq  15821  bitsres  15822  smuval2  15831  smupval  15837  smueqlem  15839  smumul  15842  1arith  16263  isstruct2  16493  setscom  16527  ressress  16562  imasvscafn  16810  imasless  16813  mrcssv  16885  isacs1i  16928  mreacs  16929  acsfn  16930  isacs4lem  17778  isacs5lem  17779  mhmima  17989  cntzmhm  18469  f1omvdconj  18574  f1omvdco2  18576  symgsssg  18595  symggen  18598  efgval  18843  gsumzaddlem  19041  gsumconst  19054  dmdprdd  19121  dprdfeq0  19144  dprdres  19150  dprdss  19151  dprdz  19152  subgdmdprd  19156  dprddisj2  19161  dprd2dlem1  19163  dprd2da  19164  dprd2d2  19166  dmdprdsplit2lem  19167  lmhmlsp  19821  lsppratlem4  19922  islbs3  19927  lbsextlem3  19932  mplcoe5  20249  mplind  20282  znleval  20701  evpmss  20730  frlmsslsp  20940  lindff1  20964  lindfrn  20965  f1lindf  20966  lindfmm  20971  lsslindf  20974  basdif0  21561  tgcl  21577  ppttop  21615  epttop  21617  ntrin  21669  mretopd  21700  neiptoptop  21739  cnclsi  21880  cnconst2  21891  cnrest2  21894  cnpresti  21896  cnprest2  21898  fiuncmp  22012  connsub  22029  connima  22033  iunconnlem  22035  1stcfb  22053  2ndc1stc  22059  2ndcdisj  22064  kgentopon  22146  llycmpkgen2  22158  1stckgenlem  22161  kgencn3  22166  ptclsg  22223  ptcnplem  22229  txtube  22248  hausdiag  22253  txkgen  22260  xkoco1cn  22265  xkoco2cn  22266  xkococnlem  22267  qtoptop2  22307  basqtop  22319  imastopn  22328  hmeores  22379  hmphdis  22404  ptcmpfi  22421  fbssfi  22445  filin  22462  infil  22471  fgtr  22498  elfm  22555  hausflim  22589  flimclslem  22592  fclscmp  22638  cnextcn  22675  tmdgsum2  22704  tgpconncomp  22721  ustexsym  22824  ustund  22830  ustimasn  22837  utoptop  22843  utopbas  22844  restutopopn  22847  blin2  23039  metustexhalf  23166  icccmplem2  23431  icccmplem3  23432  reconnlem2  23435  tcphcph  23840  fmcfil  23875  resscdrg  23961  ivthlem2  24053  ivthlem3  24054  ivth2  24056  ovolfiniun  24102  ovoliunlem1  24103  ismbl2  24128  nulmbl2  24137  unmbl  24138  shftmbl  24139  voliunlem1  24151  voliunlem2  24152  ioombl1lem4  24162  uniioombllem4  24187  uniioombllem5  24188  dyadmbllem  24200  dyadmbl  24201  mbflimsup  24267  i1fima  24279  i1fima2  24280  i1fadd  24296  itg1addlem4  24300  itg2splitlem  24349  itg2split  24350  ellimc3  24477  limcflflem  24478  limcflf  24479  limcresi  24483  limciun  24492  dvreslem  24507  dvres2lem  24508  dvres  24509  dvaddbr  24535  dvmulbr  24536  dvlip  24590  dvlip2  24592  c1liplem1  24593  dvivthlem1  24605  dvne0  24608  lhop1lem  24610  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvfsumle  24618  dvfsumabs  24620  dvfsumlem2  24624  itgsubstlem  24645  mdegleb  24658  mdeglt  24659  mdegldg  24660  mdegxrcl  24661  mdegcl  24663  ig1peu  24765  reeff1olem  25034  logccv  25246  rlimcnp2  25544  lgamgulmlem2  25607  ppisval  25681  prmdvdsfi  25684  mumul  25758  sqff1o  25759  chtlepsi  25782  chpub  25796  dchrisum0lem2a  26093  pntlem3  26185  ex-res  28220  htthlem  28694  chlejb1i  29253  ssmd2  30089  fz2ssnn0  30508  gsumle  30725  locfinreflem  31104  sibfof  31598  sitgclbn  31601  sitgaddlemb  31606  eulerpartlemgu  31635  ballotlemsima  31773  reprinrn  31889  bnj1311  32296  erdsze2lem2  32451  iccllysconn  32497  cvmopnlem  32525  msrf  32789  frpomin  33078  frrlem4  33126  frrlem13  33135  fprlem1  33137  frrlem15  33142  nosupno  33203  neiin  33680  neibastop1  33707  neibastop2lem  33708  topmeet  33712  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem19  34926  poimirlem30  34937  cnambfre  34955  itg2gt0cn  34962  sstotbnd2  35067  sstotbnd3  35069  ssbnd  35081  ismtyima  35096  heibor1lem  35102  idresssidinxp  35581  pmodlem2  36998  pmodN  37001  diaintclN  38209  djaclN  38287  dibintclN  38318  dicval  38327  dihoml4c  38527  djhcl  38551  isnacs2  39323  isnacs3  39327  diophrw  39376  pellfundre  39498  pellfundge  39499  pellfundlb  39501  pellfundglb  39502  fnwe2lem2  39671  lmhmfgima  39704  hbt  39750  cnvtrcl0  40006  trclrelexplem  40076  relexp0a  40081  rp-imass  40137  isotone2  40419  imo72b2lem1  40541  climinf  41907  islptre  41920  limccog  41921  limcleqr  41945  itgcoscmulx  42274  ismbl3  42291  ismbl4  42298  stoweidlem27  42332  dirkercncflem2  42409  fourierdlem38  42450  fourierdlem49  42460  fourierdlem51  42462  fourierdlem54  42465  fourierdlem63  42474  fourierdlem68  42479  fourierdlem69  42480  fourierdlem70  42481  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem80  42491  fourierdlem84  42495  fourierdlem85  42496  fourierdlem88  42499  fourierdlem100  42511  fourierdlem101  42512  fourierdlem104  42515  fourierdlem107  42518  fourierdlem111  42522  fourierdlem112  42523  caragenel2d  42834  hoidmv1lelem3  42895  hspmbllem3  42930  sssmf  43035  smfrec  43084  smfsuplem1  43105  mgmhmima  44089