Theorem sstrid 3945

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

Syntax hints:   → wi 4   ⊆ wss 3901

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

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

This theorem is referenced by:  difsymssdifssd  4216  wereu2  5621  sofld  6145  resssxp  6228  frpomin  6298  fimass  6682  fvmptss  6953  isofr2  7290  frxp  8068  fnse  8075  frxp2  8086  frxp3  8093  frrlem4  8231  frrlem13  8240  fprlem1  8242  smores2  8286  naddunif  8621  dffi3  9334  marypha1lem  9336  ordtypelem7  9429  ordtypelem8  9430  oismo  9445  unxpwdom2  9493  cantnfres  9586  oemapvali  9593  frmin  9661  frrlem15  9669  frrlem16  9670  tskwe  9862  acndom2  9964  dfac2a  10040  dfac12lem2  10055  cfle  10164  cofsmo  10179  coftr  10183  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  enfin1ai  10294  fin1a2lem12  10321  ttukeylem7  10425  alephexp1  10490  fpwwe2lem12  10553  fpwwe2  10554  canth4  10558  canthwelem  10561  pwfseqlem1  10569  pwfseqlem4  10573  fzossnn0  13606  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  xptrrel  14903  limsupgle  15400  limsupgre  15404  rlimres  15481  lo1res  15482  lo1resb  15487  rlimresb  15488  o1resb  15489  o1of2  15536  o1rlimmul  15542  isercolllem2  15589  isercoll  15591  climsup  15593  fprodntriv  15865  bitsinvp1  16376  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadasslem  16397  sadeq  16399  bitsres  16400  smuval2  16409  smupval  16415  smueqlem  16417  smumul  16420  1arith  16855  isstruct2  17076  setscom  17107  ressress  17174  imasvscafn  17458  imasless  17461  mrcssv  17537  isacs1i  17580  mreacs  17581  acsfn  17582  isacs4lem  18467  isacs5lem  18468  mgmhmima  18640  mhmima  18750  cntzmhm  19270  f1omvdconj  19375  f1omvdco2  19377  symgsssg  19396  symggen  19399  efgval  19646  gsumzaddlem  19850  gsumconst  19863  dmdprdd  19930  dprdfeq0  19953  dprdres  19959  dprdss  19960  dprdz  19961  subgdmdprd  19965  dprddisj2  19970  dprd2dlem1  19972  dprd2da  19973  dprd2d2  19975  dmdprdsplit2lem  19976  gsumle  20074  lmhmlsp  21001  lsppratlem4  21105  islbs3  21110  lbsextlem3  21115  znleval  21509  evpmss  21541  frlmsslsp  21751  lindff1  21775  lindfrn  21776  f1lindf  21777  lindfmm  21782  lsslindf  21785  mplcoe5  21995  mplind  22025  basdif0  22897  tgcl  22913  ppttop  22951  epttop  22953  ntrin  23005  mretopd  23036  neiptoptop  23075  cnclsi  23216  cnconst2  23227  cnrest2  23230  cnpresti  23232  cnprest2  23234  fiuncmp  23348  connsub  23365  connima  23369  iunconnlem  23371  1stcfb  23389  2ndc1stc  23395  2ndcdisj  23400  kgentopon  23482  llycmpkgen2  23494  1stckgenlem  23497  kgencn3  23502  ptclsg  23559  ptcnplem  23565  txtube  23584  hausdiag  23589  txkgen  23596  xkoco1cn  23601  xkoco2cn  23602  xkococnlem  23603  qtoptop2  23643  basqtop  23655  imastopn  23664  hmeores  23715  hmphdis  23740  ptcmpfi  23757  fbssfi  23781  filin  23798  infil  23807  fgtr  23834  elfm  23891  hausflim  23925  flimclslem  23928  fclscmp  23974  cnextcn  24011  tmdgsum2  24040  tgpconncomp  24057  ustexsym  24160  ustund  24166  ustimasn  24172  utoptop  24178  utopbas  24179  restutopopn  24182  blin2  24373  metustexhalf  24500  icccmplem2  24768  icccmplem3  24769  reconnlem2  24772  tcphcph  25193  fmcfil  25228  resscdrg  25314  ivthlem2  25409  ivthlem3  25410  ivth2  25412  ovolfiniun  25458  ovoliunlem1  25459  ismbl2  25484  nulmbl2  25493  unmbl  25494  shftmbl  25495  voliunlem1  25507  voliunlem2  25508  ioombl1lem4  25518  uniioombllem4  25543  uniioombllem5  25544  dyadmbllem  25556  dyadmbl  25557  mbflimsup  25623  i1fima  25635  i1fima2  25636  i1fadd  25652  itg1addlem4  25656  itg2splitlem  25705  itg2split  25706  ellimc3  25836  limcflflem  25837  limcflf  25838  limcresi  25842  limciun  25851  dvreslem  25866  dvres2lem  25867  dvres  25868  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvlip  25954  dvlip2  25956  c1liplem1  25957  dvivthlem1  25969  dvne0  25972  lhop1lem  25974  lhop  25977  dvcnvrelem1  25978  dvcnvrelem2  25979  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  itgsubstlem  26011  mdegleb  26025  mdeglt  26026  mdegldg  26027  mdegxrcl  26028  mdegcl  26030  ig1peu  26136  reeff1olem  26412  logccv  26628  rlimcnp2  26932  lgamgulmlem2  26996  ppisval  27070  prmdvdsfi  27073  mumul  27147  sqff1o  27148  chtlepsi  27173  chpub  27187  dchrisum0lem2a  27484  pntlem3  27576  nosupno  27671  noetalem1  27709  cutlt  27928  negsproplem2  28025  onsbnd  28277  ex-res  30516  htthlem  30992  chlejb1i  31551  ssmd2  32387  fz2ssnn0  32865  gsumpart  33146  gsumhashmul  33150  elrgspnsubrunlem2  33330  extvfvcl  33701  mplvrpmrhm  33712  esplyind  33731  vietalem  33735  locfinreflem  33997  sibfof  34497  sitgclbn  34500  sitgaddlemb  34505  eulerpartlemgu  34534  ballotlemsima  34673  reprinrn  34775  bnj1311  35180  fnrelpredd  35247  erdsze2lem2  35398  iccllysconn  35444  cvmopnlem  35472  msrf  35736  neiin  36526  neibastop1  36553  neibastop2lem  36554  topmeet  36558  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem19  37836  poimirlem30  37847  cnambfre  37865  itg2gt0cn  37872  sstotbnd2  37971  sstotbnd3  37973  ssbnd  37985  ismtyima  38000  heibor1lem  38006  idresssidinxp  38503  pmodlem2  40103  pmodN  40106  diaintclN  41314  djaclN  41392  dibintclN  41423  dicval  41432  dihoml4c  41632  djhcl  41656  infdesc  42882  isnacs2  42944  isnacs3  42948  diophrw  42997  pellfundre  43119  pellfundge  43120  pellfundlb  43122  pellfundglb  43123  fnwe2lem2  43289  lmhmfgima  43322  hbt  43368  omabs2  43570  nadd2rabord  43623  nadd1rabord  43627  cnvtrcl0  43863  trclrelexplem  43948  relexp0a  43953  isotone2  44286  imo72b2lem1  44406  tcfr  45200  modelaxreplem1  45215  wfac8prim  45239  climinf  45848  islptre  45861  limccog  45862  limcleqr  45884  limsupvaluz2  45978  itgcoscmulx  46209  ismbl3  46226  ismbl4  46233  stoweidlem27  46267  dirkercncflem2  46344  fourierdlem38  46385  fourierdlem49  46395  fourierdlem51  46397  fourierdlem54  46400  fourierdlem63  46409  fourierdlem68  46414  fourierdlem69  46415  fourierdlem70  46416  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem80  46426  fourierdlem84  46430  fourierdlem85  46431  fourierdlem88  46434  fourierdlem100  46446  fourierdlem101  46447  fourierdlem104  46450  fourierdlem107  46453  fourierdlem111  46457  fourierdlem112  46458  caragenel2d  46772  hoidmv1lelem3  46833  hspmbllem3  46868  sssmf  46978  smfrec  47029  smfsuplem1  47051