Theorem sstrdi 3946

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 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:  difss2  4090  rintn0  5064  eqbrrdva  5818  ssxpb  6132  resssxp  6228  relfld  6233  funssxp  6690  dff2  7044  dff3  7045  fliftf  7261  1stcof  7963  2ndcof  7964  frxp2  8086  frxp3  8093  frrlem13  8240  nnunifi  9191  elfiun  9333  marypha1lem  9336  marypha1  9337  ordtypelem7  9429  tcmin  9648  unwf  9722  rankfu  9789  tcrank  9796  aceq3lem  10030  dfac12lem2  10055  ackbij1lem9  10137  ackbij1lem10  10138  ackbij1lem16  10144  fin23lem26  10235  fin23lem27  10238  fin1a2lem6  10315  itunitc  10331  axdc3lem2  10361  ttukeylem5  10423  fpwwe2lem12  10553  canthwelem  10561  pwfseqlem4  10573  wunex2  10649  wunex3  10652  inar1  10686  inatsk  10689  gruina  10729  suprfinzcl  12606  suprzub  12852  uzsupss  12853  uzwo3  12856  rpnnen1lem4  12893  rpnnen1lem5  12894  supxrre  13242  infxrre  13252  ioodisj  13398  supicclub2  13420  fzssnn  13484  fzossnn0  13606  elfzom1elp1fzo  13648  injresinjlem  13706  uzindi  13905  ssnn0fi  13908  seqcoll  14387  seqcoll2  14388  reltrclfv  14940  relexpdmg  14965  relexpdm  14966  relexprng  14969  relexprn  14970  relexpfld  14972  relexpaddg  14976  limsupval2  15403  limsupgre  15404  limsupbnd2  15406  rlimuni  15473  rlimcld2  15501  rlimno1  15577  isercolllem2  15589  isercoll  15591  summolem2a  15638  summolem2  15639  fsumsers  15651  fsumcvg3  15652  prodmolem2a  15857  prodmolem2  15858  zprod  15860  lcmfnnval  16551  lcmfnncl  16556  prmdvdsbc  16653  4sqlem11  16883  vdwlem8  16916  vdwlem11  16919  ramub2  16942  0ram  16948  0ram2  16949  0ramcl  16951  ramub1lem2  16955  prmgaplem3  16981  prmgaplem4  16982  isohom  17700  funcres2c  17827  resscntz  19262  cntzidss  19269  cntzmhm2  19271  pgpssslw  19543  cntzspan  19773  gsumval3  19836  gsum2d  19901  dprdspan  19958  dprdres  19959  subdrgint  20736  sdrgint  20737  primefld  20738  lssintcl  20915  lbsextlem2  21114  lbsextlem3  21115  lbsextlem4  21116  islinds3  21789  fctop  22948  cctop  22950  neitr  23124  ordtbas2  23135  ordtopn1  23138  ordtopn2  23139  lmss  23242  clsconn  23374  2ndcdisj  23400  2ndcomap  23402  ptbasfi  23525  txcmplem2  23586  hausdiag  23589  txkgen  23596  basqtop  23655  alexsubb  23990  alexsubALTlem4  23994  tsmsres  24088  tsmsxplem1  24097  tsmsxp  24099  ustrel  24156  utop3cls  24195  prdsmet  24314  metustrel  24496  icccmplem2  24768  xrge0tsms  24779  cnmptre  24877  icchmeo  24894  icchmeoOLD  24895  bndth  24913  lebnumlem2  24917  cfilresi  25251  causs  25254  bcthlem5  25284  evthicc  25416  ovolficcss  25426  ovolmge0  25434  ovolgelb  25437  ovollb2lem  25445  ovollb2  25446  ovolunlem1a  25453  ovolunlem1  25454  ovoliunlem1  25459  ovoliunlem2  25460  ovoliun  25462  ovolscalem1  25470  ovolicc1  25473  ovolicc2lem4  25477  ovolicc2  25479  voliunlem2  25508  voliunlem3  25509  ioombl1lem2  25516  ioombl1lem4  25518  uniioovol  25536  uniiccvol  25537  uniioombllem1  25538  uniioombllem2  25540  uniioombllem3  25542  uniioombllem4  25543  uniioombllem6  25545  dyadmbllem  25556  dyadmbl  25557  volcn  25563  vitalilem4  25568  vitalilem5  25569  cnmbf  25616  i1fmul  25653  itg1addlem4  25656  itg2seq  25699  dvbssntr  25857  dvreslem  25866  dvcjbr  25909  dvferm1  25945  dvferm2  25947  cmvth  25951  cmvthOLD  25952  dvlip  25954  lhop1lem  25974  lhop2  25976  lhop  25977  dvcnvrelem2  25979  dvcnvre  25980  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  ftc1a  26000  ftc1lem3  26001  ftc1lem6  26004  itgsubstlem  26011  itgpowd  26013  mdegleb  26025  mdeglt  26026  mdegldg  26027  mdegxrcl  26028  mdegcl  26030  deg1mul3le  26078  ig1pdvds  26141  plyeq0lem  26171  aannenlem2  26293  aalioulem3  26298  taylf  26324  taylthlem2  26338  taylthlem2OLD  26339  pserulm  26387  psercn2  26388  psercn2OLD  26389  psercn  26392  reeff1olem  26412  efcvx  26415  loglesqrt  26727  rlimcnp  26931  xrlimcnp  26934  jensen  26955  wilthlem2  27035  vmadivsumb  27450  pntrsumo1  27532  pntlem3  27576  noseqrdgfn  28302  bdaypw2n0bndlem  28459  perpln2  28783  axcontlem10  29046  usgrexmplef  29332  dfpth2  29802  nmoxr  30841  nmooge0  30842  nmoolb  30846  nmoubi  30847  ubthlem1  30945  shmodi  31465  nmopxr  31941  nmfnxr  31954  nmoplb  31982  nmopub  31983  nmfnlb  31999  nmfnleub  32000  nmopun  32089  branmfn  32180  mdslj1i  32394  hatomistici  32437  xppreima2  32729  fsuppcurry1  32803  fsuppcurry2  32804  fpwrelmap  32812  infxrge0gelb  32846  gsumpart  33146  xrge0tsmsd  33155  pmtrcnel2  33172  cyc3genpm  33234  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  1fldgenq  33404  ssdifidllem  33537  ssmxidllem  33554  mplmulmvr  33704  zarcmplem  34038  metideq  34050  metider  34051  pstmfval  34053  esumgect  34247  esum2d  34250  sigaclci  34289  insiga  34294  omssubadd  34457  eulerpartlemgs2  34537  ballotlemsima  34673  signsply0  34708  iblidicc  34749  fsum2dsub  34764  reprsuc  34772  reprgt  34778  bnj1145  35149  bnj1137  35151  bnj1136  35153  resconn  35440  cvmliftlem8  35486  cvmlift3lem6  35518  mclsssvlem  35756  mclsind  35764  mclsppslem  35777  ivthALT  36529  neibastop1  36553  topjoin  36559  bj-imdirco  37395  ptrecube  37821  poimirlem6  37827  poimirlem15  37836  heicant  37856  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  itg2gt0cn  37876  ftc1cnnc  37893  ftc1anclem3  37896  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  areacirclem2  37910  areacirclem3  37911  areacirclem4  37912  totbndbnd  37990  prdsbnd  37994  heiborlem1  38012  rrnequiv  38036  reheibor  38040  iccbnd  38041  pmapssbaN  40020  2polssN  40175  paddunN  40187  poldmj1N  40188  ispsubcl2N  40207  psubclinN  40208  paddatclN  40209  poml4N  40213  diaglbN  41315  diaintclN  41318  dibglbN  41426  dibintclN  41427  dicssdvh  41446  dihvalrel  41539  dochexmidlem4  41723  infdesc  42886  ttac  43278  hbtlem6  43371  hbt  43372  cnvssb  43827  cnvrcl0  43866  cnvtrrel  43911  relexpaddss  43959  cotrcltrcl  43966  cotrclrcl  43983  frege96d  43990  frege97d  43993  frege109d  43998  frege131d  44005  rfovcnvf1od  44245  isotone2  44290  gneispace  44375  k0004ss1  44392  grumnudlem  44526  uzfissfz  45571  suplesup  45584  ssrexr  45676  limciccioolb  45867  limcicciooub  45881  limcleqr  45888  cnrefiisplem  46073  cncfiooicclem1  46137  ibliccsinexp  46195  iblioosinexp  46197  itgcoscmulx  46213  itgsincmulx  46218  itgsubsticclem  46219  itgiccshift  46224  itgperiod  46225  itgsbtaddcnst  46226  stoweidlem34  46278  stoweidlem59  46303  dirkeritg  46346  dirkercncflem2  46348  fourierdlem20  46371  fourierdlem31  46382  fourierdlem39  46390  fourierdlem42  46393  fourierdlem46  46396  fourierdlem52  46402  fourierdlem53  46403  fourierdlem60  46410  fourierdlem61  46411  fourierdlem62  46412  fourierdlem68  46418  fourierdlem76  46426  fourierdlem85  46435  fourierdlem88  46438  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem93  46443  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fouriersw  46475  etransclem46  46524  etransclem48  46526  sge0less  46636  sge0resplit  46650  sge0isum  46671  pimdecfgtioo  46961  pimincfltioo  46962  iccpartipre  47667  bgoldbtbndlem2  48052  setrec1lem4  49935  setrec2fun  49937