Theorem sstrdi 3927

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sstrdi.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sstrdi.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
sstrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrdi

Step	Hyp	Ref	Expression
1		sstrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrdi.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	sstrd 3925	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  difss2  4061  rintn0  4994  eqbrrdva  5704  ssxpb  5998  resssxp  6089  relfld  6094  funssxp  6509  dff2  6842  dff3  6843  fliftf  7047  1stcof  7701  2ndcof  7702  nnunifi  8753  elfiun  8878  marypha1lem  8881  marypha1  8882  ordtypelem7  8972  tcmin  9167  unwf  9223  rankfu  9290  tcrank  9297  aceq3lem  9531  dfac12lem2  9555  ackbij1lem9  9639  ackbij1lem10  9640  ackbij1lem16  9646  fin23lem26  9736  fin23lem27  9739  fin1a2lem6  9816  itunitc  9832  axdc3lem2  9862  ttukeylem5  9924  fpwwe2lem13  10053  canthwelem  10061  pwfseqlem4  10073  wunex2  10149  wunex3  10152  inar1  10186  inatsk  10189  gruina  10229  suprfinzcl  12085  suprzub  12327  uzsupss  12328  uzwo3  12331  rpnnen1lem4  12367  rpnnen1lem5  12368  supxrre  12708  infxrre  12717  ioodisj  12860  supicclub2  12882  fzssnn  12946  fzossnn0  13063  elfzom1elp1fzo  13099  injresinjlem  13152  uzindi  13345  ssnn0fi  13348  seqcoll  13818  seqcoll2  13819  reltrclfv  14368  relexpdmg  14393  relexpdm  14394  relexprng  14397  relexprn  14398  relexpfld  14400  relexpaddg  14404  limsupval2  14829  limsupgre  14830  limsupbnd2  14832  rlimuni  14899  rlimcld2  14927  rlimno1  15002  isercolllem2  15014  isercoll  15016  summolem2a  15064  summolem2  15065  fsumsers  15077  fsumcvg3  15078  prodmolem2a  15280  prodmolem2  15281  zprod  15283  lcmfnnval  15958  lcmfnncl  15963  4sqlem11  16281  vdwlem8  16314  vdwlem11  16317  ramub2  16340  0ram  16346  0ram2  16347  0ramcl  16349  ramub1lem2  16353  prmgaplem3  16379  prmgaplem4  16380  isohom  17038  funcres2c  17163  resscntz  18454  cntzidss  18460  cntzmhm2  18462  pgpssslw  18731  cntzspan  18957  gsumval3  19020  gsum2d  19085  dprdspan  19142  dprdres  19143  subdrgint  19575  sdrgint  19576  primefld  19577  lssintcl  19729  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  islinds3  20523  fctop  21609  cctop  21611  neitr  21785  ordtbas2  21796  ordtopn1  21799  ordtopn2  21800  lmss  21903  clsconn  22035  2ndcdisj  22061  2ndcomap  22063  ptbasfi  22186  txcmplem2  22247  hausdiag  22250  txkgen  22257  basqtop  22316  alexsubb  22651  alexsubALTlem4  22655  tsmsres  22749  tsmsxplem1  22758  tsmsxp  22760  ustrel  22817  utop3cls  22857  prdsmet  22977  metustrel  23159  icccmplem2  23428  xrge0tsms  23439  cnmptre  23532  icchmeo  23546  bndth  23563  lebnumlem2  23567  cfilresi  23899  causs  23902  bcthlem5  23932  evthicc  24063  ovolficcss  24073  ovolmge0  24081  ovolgelb  24084  ovollb2lem  24092  ovollb2  24093  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliunlem2  24107  ovoliun  24109  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem4  24124  ovolicc2  24126  voliunlem2  24155  voliunlem3  24156  ioombl1lem2  24163  ioombl1lem4  24165  uniioovol  24183  uniiccvol  24184  uniioombllem1  24185  uniioombllem2  24187  uniioombllem3  24189  uniioombllem4  24190  uniioombllem6  24192  dyadmbllem  24203  dyadmbl  24204  volcn  24210  vitalilem4  24215  vitalilem5  24216  cnmbf  24263  i1fmul  24300  itg1addlem4  24303  itg2seq  24346  dvbssntr  24503  dvreslem  24512  dvcjbr  24552  dvferm1  24588  dvferm2  24590  cmvth  24594  dvlip  24596  lhop1lem  24616  lhop2  24618  lhop  24619  dvcnvrelem2  24621  dvcnvre  24622  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  dvfsumlem2  24630  ftc1a  24640  ftc1lem3  24641  ftc1lem6  24644  itgsubstlem  24651  itgpowd  24653  mdegleb  24665  mdeglt  24666  mdegldg  24667  mdegxrcl  24668  mdegcl  24670  deg1mul3le  24717  ig1pdvds  24777  plyeq0lem  24807  aannenlem2  24925  aalioulem3  24930  taylf  24956  taylthlem2  24969  pserulm  25017  psercn2  25018  psercn  25021  reeff1olem  25041  efcvx  25044  loglesqrt  25347  rlimcnp  25551  xrlimcnp  25554  jensen  25574  wilthlem2  25654  vmadivsumb  26067  pntrsumo1  26149  pntlem3  26193  perpln2  26505  axcontlem10  26767  usgrexmplef  27049  nmoxr  28549  nmooge0  28550  nmoolb  28554  nmoubi  28555  ubthlem1  28653  shmodi  29173  nmopxr  29649  nmfnxr  29662  nmoplb  29690  nmopub  29691  nmfnlb  29707  nmfnleub  29708  nmopun  29797  branmfn  29888  mdslj1i  30102  hatomistici  30145  xppreima2  30413  fsuppcurry1  30487  fsuppcurry2  30488  fpwrelmap  30495  infxrge0gelb  30516  prmdvdsbc  30558  gsumpart  30740  xrge0tsmsd  30742  pmtrcnel2  30784  cyc3genpm  30844  ssmxidllem  31049  zarcmplem  31234  metideq  31246  metider  31247  pstmfval  31249  esumgect  31459  esum2d  31462  sigaclci  31501  insiga  31506  omssubadd  31668  eulerpartlemgs2  31748  ballotlemsima  31883  signsply0  31931  iblidicc  31973  fsum2dsub  31988  reprsuc  31996  reprgt  32002  bnj1145  32375  bnj1137  32377  bnj1136  32379  resconn  32606  cvmliftlem8  32652  cvmlift3lem6  32684  mclsssvlem  32922  mclsind  32930  mclsppslem  32943  frrlem13  33248  nosupbday  33318  ivthALT  33796  neibastop1  33820  topjoin  33826  bj-imdirco  34605  ptrecube  35057  poimirlem6  35063  poimirlem15  35072  heicant  35092  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  itg2gt0cn  35112  ftc1cnnc  35129  ftc1anclem3  35132  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  areacirclem2  35146  areacirclem3  35147  areacirclem4  35148  totbndbnd  35227  prdsbnd  35231  heiborlem1  35249  rrnequiv  35273  reheibor  35277  iccbnd  35278  pmapssbaN  37056  2polssN  37211  paddunN  37223  poldmj1N  37224  ispsubcl2N  37243  psubclinN  37244  paddatclN  37245  poml4N  37249  diaglbN  38351  diaintclN  38354  dibglbN  38462  dibintclN  38463  dicssdvh  38482  dihvalrel  38575  dochexmidlem4  38759  rmxyelqirr  39851  ttac  39977  hbtlem6  40073  hbt  40074  cnvssb  40286  cnvrcl0  40325  cnvtrrel  40371  relexpaddss  40419  cotrcltrcl  40426  cotrclrcl  40443  frege96d  40450  frege97d  40453  frege109d  40458  frege131d  40465  rfovcnvf1od  40705  isotone2  40752  gneispace  40837  k0004ss1  40854  grumnudlem  40993  uzfissfz  41958  suplesup  41971  ssrexr  42069  limciccioolb  42263  limcicciooub  42279  limcleqr  42286  cnrefiisplem  42471  cncfiooicclem1  42535  ibliccsinexp  42593  iblioosinexp  42595  itgcoscmulx  42611  itgsincmulx  42616  itgsubsticclem  42617  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stoweidlem34  42676  stoweidlem59  42701  dirkeritg  42744  dirkercncflem2  42746  fourierdlem20  42769  fourierdlem31  42780  fourierdlem39  42788  fourierdlem42  42791  fourierdlem46  42794  fourierdlem52  42800  fourierdlem53  42801  fourierdlem60  42808  fourierdlem61  42809  fourierdlem62  42810  fourierdlem68  42816  fourierdlem76  42824  fourierdlem85  42833  fourierdlem88  42836  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem93  42841  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fouriersw  42873  etransclem46  42922  etransclem48  42924  sge0less  43031  sge0resplit  43045  sge0isum  43066  pimdecfgtioo  43352  pimincfltioo  43353  iccpartipre  43938  bgoldbtbndlem2  44324  setrec1lem4  45220  setrec2fun  45222