Theorem sstrid 3928

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

Syntax hints:   → wi 4   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  difsymssdifssd  4184  wereu2  5577  sofld  6079  resssxp  6162  frpomin  6228  fimass  6605  fvmptss  6869  fimacnvOLD  6930  isofr2  7195  frxp  7938  fnse  7945  frrlem4  8076  frrlem13  8085  fprlem1  8087  smores2  8156  dffi3  9120  marypha1lem  9122  ordtypelem7  9213  ordtypelem8  9214  oismo  9229  unxpwdom2  9277  cantnfres  9365  oemapvali  9372  frrlem15  9446  tskwe  9639  acndom2  9741  dfac2a  9816  dfac12lem2  9831  cfle  9941  cofsmo  9956  coftr  9960  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  enfin1ai  10071  fin1a2lem12  10098  ttukeylem7  10202  alephexp1  10266  fpwwe2lem12  10329  fpwwe2  10330  canth4  10334  canthwelem  10337  pwfseqlem1  10345  pwfseqlem4  10349  fzossnn0  13346  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  xptrrel  14619  limsupgle  15114  limsupgre  15118  rlimres  15195  lo1res  15196  lo1resb  15201  rlimresb  15202  o1resb  15203  o1of2  15250  o1rlimmul  15256  isercolllem2  15305  isercoll  15307  climsup  15309  fprodntriv  15580  bitsinvp1  16084  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadasslem  16105  sadeq  16107  bitsres  16108  smuval2  16117  smupval  16123  smueqlem  16125  smumul  16128  1arith  16556  isstruct2  16778  setscom  16809  ressress  16884  imasvscafn  17165  imasless  17168  mrcssv  17240  isacs1i  17283  mreacs  17284  acsfn  17285  isacs4lem  18177  isacs5lem  18178  mhmima  18378  cntzmhm  18860  f1omvdconj  18969  f1omvdco2  18971  symgsssg  18990  symggen  18993  efgval  19238  gsumzaddlem  19437  gsumconst  19450  dmdprdd  19517  dprdfeq0  19540  dprdres  19546  dprdss  19547  dprdz  19548  subgdmdprd  19552  dprddisj2  19557  dprd2dlem1  19559  dprd2da  19560  dprd2d2  19562  dmdprdsplit2lem  19563  lmhmlsp  20226  lsppratlem4  20327  islbs3  20332  lbsextlem3  20337  znleval  20674  evpmss  20703  frlmsslsp  20913  lindff1  20937  lindfrn  20938  f1lindf  20939  lindfmm  20944  lsslindf  20947  mplcoe5  21151  mplind  21188  basdif0  22011  tgcl  22027  ppttop  22065  epttop  22067  ntrin  22120  mretopd  22151  neiptoptop  22190  cnclsi  22331  cnconst2  22342  cnrest2  22345  cnpresti  22347  cnprest2  22349  fiuncmp  22463  connsub  22480  connima  22484  iunconnlem  22486  1stcfb  22504  2ndc1stc  22510  2ndcdisj  22515  kgentopon  22597  llycmpkgen2  22609  1stckgenlem  22612  kgencn3  22617  ptclsg  22674  ptcnplem  22680  txtube  22699  hausdiag  22704  txkgen  22711  xkoco1cn  22716  xkoco2cn  22717  xkococnlem  22718  qtoptop2  22758  basqtop  22770  imastopn  22779  hmeores  22830  hmphdis  22855  ptcmpfi  22872  fbssfi  22896  filin  22913  infil  22922  fgtr  22949  elfm  23006  hausflim  23040  flimclslem  23043  fclscmp  23089  cnextcn  23126  tmdgsum2  23155  tgpconncomp  23172  ustexsym  23275  ustund  23281  ustimasn  23288  utoptop  23294  utopbas  23295  restutopopn  23298  blin2  23490  metustexhalf  23618  icccmplem2  23892  icccmplem3  23893  reconnlem2  23896  tcphcph  24306  fmcfil  24341  resscdrg  24427  ivthlem2  24521  ivthlem3  24522  ivth2  24524  ovolfiniun  24570  ovoliunlem1  24571  ismbl2  24596  nulmbl2  24605  unmbl  24606  shftmbl  24607  voliunlem1  24619  voliunlem2  24620  ioombl1lem4  24630  uniioombllem4  24655  uniioombllem5  24656  dyadmbllem  24668  dyadmbl  24669  mbflimsup  24735  i1fima  24747  i1fima2  24748  i1fadd  24764  itg1addlem4  24768  itg1addlem4OLD  24769  itg2splitlem  24818  itg2split  24819  ellimc3  24948  limcflflem  24949  limcflf  24950  limcresi  24954  limciun  24963  dvreslem  24978  dvres2lem  24979  dvres  24980  dvaddbr  25007  dvmulbr  25008  dvlip  25062  dvlip2  25064  c1liplem1  25065  dvivthlem1  25077  dvne0  25080  lhop1lem  25082  lhop  25085  dvcnvrelem1  25086  dvcnvrelem2  25087  dvfsumle  25090  dvfsumabs  25092  dvfsumlem2  25096  itgsubstlem  25117  mdegleb  25134  mdeglt  25135  mdegldg  25136  mdegxrcl  25137  mdegcl  25139  ig1peu  25241  reeff1olem  25510  logccv  25723  rlimcnp2  26021  lgamgulmlem2  26084  ppisval  26158  prmdvdsfi  26161  mumul  26235  sqff1o  26236  chtlepsi  26259  chpub  26273  dchrisum0lem2a  26570  pntlem3  26662  ex-res  28706  htthlem  29180  chlejb1i  29739  ssmd2  30575  fz2ssnn0  31008  gsumpart  31217  gsumhashmul  31218  gsumle  31252  locfinreflem  31692  sibfof  32207  sitgclbn  32210  sitgaddlemb  32215  eulerpartlemgu  32244  ballotlemsima  32382  reprinrn  32498  bnj1311  32904  fnrelpredd  32961  erdsze2lem2  33066  iccllysconn  33112  cvmopnlem  33140  msrf  33404  frxp2  33718  frxp3  33724  nosupno  33833  noetalem1  33871  neiin  34448  neibastop1  34475  neibastop2lem  34476  topmeet  34480  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem19  35723  poimirlem30  35734  cnambfre  35752  itg2gt0cn  35759  sstotbnd2  35859  sstotbnd3  35861  ssbnd  35873  ismtyima  35888  heibor1lem  35894  idresssidinxp  36371  pmodlem2  37788  pmodN  37791  diaintclN  38999  djaclN  39077  dibintclN  39108  dicval  39117  dihoml4c  39317  djhcl  39341  infdesc  40396  isnacs2  40444  isnacs3  40448  diophrw  40497  pellfundre  40619  pellfundge  40620  pellfundlb  40622  pellfundglb  40623  fnwe2lem2  40792  lmhmfgima  40825  hbt  40871  cnvtrcl0  41123  trclrelexplem  41208  relexp0a  41213  isotone2  41548  imo72b2lem1  41669  climinf  43037  islptre  43050  limccog  43051  limcleqr  43075  itgcoscmulx  43400  ismbl3  43417  ismbl4  43424  stoweidlem27  43458  dirkercncflem2  43535  fourierdlem38  43576  fourierdlem49  43586  fourierdlem51  43588  fourierdlem54  43591  fourierdlem63  43600  fourierdlem68  43605  fourierdlem69  43606  fourierdlem70  43607  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem84  43621  fourierdlem85  43622  fourierdlem88  43625  fourierdlem100  43637  fourierdlem101  43638  fourierdlem104  43641  fourierdlem107  43644  fourierdlem111  43648  fourierdlem112  43649  caragenel2d  43960  hoidmv1lelem3  44021  hspmbllem3  44056  sssmf  44161  smfrec  44210  smfsuplem1  44231  mgmhmima  45244