Theorem sstrdi 3976

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

Syntax hints:   → wi 4   ⊆ wss 3931

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

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

This theorem is referenced by:  difss2  4118  rintn0  5090  eqbrrdva  5854  ssxpb  6168  resssxp  6264  relfld  6269  funssxp  6739  dff2  7094  dff3  7095  fliftf  7313  1stcof  8023  2ndcof  8024  frxp2  8148  frxp3  8155  frrlem13  8302  nnunifi  9304  elfiun  9447  marypha1lem  9450  marypha1  9451  ordtypelem7  9543  tcmin  9760  unwf  9829  rankfu  9896  tcrank  9903  aceq3lem  10139  dfac12lem2  10164  ackbij1lem9  10246  ackbij1lem10  10247  ackbij1lem16  10253  fin23lem26  10344  fin23lem27  10347  fin1a2lem6  10424  itunitc  10440  axdc3lem2  10470  ttukeylem5  10532  fpwwe2lem12  10661  canthwelem  10669  pwfseqlem4  10681  wunex2  10757  wunex3  10760  inar1  10794  inatsk  10797  gruina  10837  suprfinzcl  12712  suprzub  12960  uzsupss  12961  uzwo3  12964  rpnnen1lem4  13001  rpnnen1lem5  13002  supxrre  13348  infxrre  13358  ioodisj  13504  supicclub2  13526  fzssnn  13590  fzossnn0  13712  elfzom1elp1fzo  13753  injresinjlem  13808  uzindi  14005  ssnn0fi  14008  seqcoll  14487  seqcoll2  14488  reltrclfv  15041  relexpdmg  15066  relexpdm  15067  relexprng  15070  relexprn  15071  relexpfld  15073  relexpaddg  15077  limsupval2  15501  limsupgre  15502  limsupbnd2  15504  rlimuni  15571  rlimcld2  15599  rlimno1  15675  isercolllem2  15687  isercoll  15689  summolem2a  15736  summolem2  15737  fsumsers  15749  fsumcvg3  15750  prodmolem2a  15955  prodmolem2  15956  zprod  15958  lcmfnnval  16648  lcmfnncl  16653  prmdvdsbc  16750  4sqlem11  16980  vdwlem8  17013  vdwlem11  17016  ramub2  17039  0ram  17045  0ram2  17046  0ramcl  17048  ramub1lem2  17052  prmgaplem3  17078  prmgaplem4  17079  isohom  17794  funcres2c  17921  resscntz  19321  cntzidss  19328  cntzmhm2  19330  pgpssslw  19600  cntzspan  19830  gsumval3  19893  gsum2d  19958  dprdspan  20015  dprdres  20016  subdrgint  20768  sdrgint  20769  primefld  20770  lssintcl  20926  lbsextlem2  21125  lbsextlem3  21126  lbsextlem4  21127  islinds3  21799  fctop  22947  cctop  22949  neitr  23123  ordtbas2  23134  ordtopn1  23137  ordtopn2  23138  lmss  23241  clsconn  23373  2ndcdisj  23399  2ndcomap  23401  ptbasfi  23524  txcmplem2  23585  hausdiag  23588  txkgen  23595  basqtop  23654  alexsubb  23989  alexsubALTlem4  23993  tsmsres  24087  tsmsxplem1  24096  tsmsxp  24098  ustrel  24155  utop3cls  24195  prdsmet  24314  metustrel  24496  icccmplem2  24768  xrge0tsms  24779  cnmptre  24877  icchmeo  24894  icchmeoOLD  24895  bndth  24913  lebnumlem2  24917  cfilresi  25252  causs  25255  bcthlem5  25285  evthicc  25417  ovolficcss  25427  ovolmge0  25435  ovolgelb  25438  ovollb2lem  25446  ovollb2  25447  ovolunlem1a  25454  ovolunlem1  25455  ovoliunlem1  25460  ovoliunlem2  25461  ovoliun  25463  ovolscalem1  25471  ovolicc1  25474  ovolicc2lem4  25478  ovolicc2  25480  voliunlem2  25509  voliunlem3  25510  ioombl1lem2  25517  ioombl1lem4  25519  uniioovol  25537  uniiccvol  25538  uniioombllem1  25539  uniioombllem2  25541  uniioombllem3  25543  uniioombllem4  25544  uniioombllem6  25546  dyadmbllem  25557  dyadmbl  25558  volcn  25564  vitalilem4  25569  vitalilem5  25570  cnmbf  25617  i1fmul  25654  itg1addlem4  25657  itg2seq  25700  dvbssntr  25858  dvreslem  25867  dvcjbr  25910  dvferm1  25946  dvferm2  25948  cmvth  25952  cmvthOLD  25953  dvlip  25955  lhop1lem  25975  lhop2  25977  lhop  25978  dvcnvrelem2  25980  dvcnvre  25981  dvfsumle  25983  dvfsumleOLD  25984  dvfsumge  25985  dvfsumabs  25986  dvfsumlem2  25990  dvfsumlem2OLD  25991  ftc1a  26001  ftc1lem3  26002  ftc1lem6  26005  itgsubstlem  26012  itgpowd  26014  mdegleb  26026  mdeglt  26027  mdegldg  26028  mdegxrcl  26029  mdegcl  26031  deg1mul3le  26079  ig1pdvds  26142  plyeq0lem  26172  aannenlem2  26294  aalioulem3  26299  taylf  26325  taylthlem2  26339  taylthlem2OLD  26340  pserulm  26388  psercn2  26389  psercn2OLD  26390  psercn  26393  reeff1olem  26413  efcvx  26416  loglesqrt  26728  rlimcnp  26932  xrlimcnp  26935  jensen  26956  wilthlem2  27036  vmadivsumb  27451  pntrsumo1  27533  pntlem3  27577  noseqrdgfn  28257  perpln2  28695  axcontlem10  28957  usgrexmplef  29243  dfpth2  29716  nmoxr  30752  nmooge0  30753  nmoolb  30757  nmoubi  30758  ubthlem1  30856  shmodi  31376  nmopxr  31852  nmfnxr  31865  nmoplb  31893  nmopub  31894  nmfnlb  31910  nmfnleub  31911  nmopun  32000  branmfn  32091  mdslj1i  32305  hatomistici  32348  xppreima2  32634  fsuppcurry1  32707  fsuppcurry2  32708  fpwrelmap  32715  infxrge0gelb  32748  gsumpart  33056  xrge0tsmsd  33061  pmtrcnel2  33106  cyc3genpm  33168  elrgspnsubrunlem1  33247  elrgspnsubrunlem2  33248  1fldgenq  33321  ssdifidllem  33476  ssmxidllem  33493  zarcmplem  33917  metideq  33929  metider  33930  pstmfval  33932  esumgect  34126  esum2d  34129  sigaclci  34168  insiga  34173  omssubadd  34337  eulerpartlemgs2  34417  ballotlemsima  34553  signsply0  34588  iblidicc  34629  fsum2dsub  34644  reprsuc  34652  reprgt  34658  bnj1145  35029  bnj1137  35031  bnj1136  35033  resconn  35273  cvmliftlem8  35319  cvmlift3lem6  35351  mclsssvlem  35589  mclsind  35597  mclsppslem  35610  ivthALT  36358  neibastop1  36382  topjoin  36388  bj-imdirco  37213  ptrecube  37649  poimirlem6  37655  poimirlem15  37664  heicant  37684  mblfinlem2  37687  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  itg2gt0cn  37704  ftc1cnnc  37721  ftc1anclem3  37724  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  areacirclem2  37738  areacirclem3  37739  areacirclem4  37740  totbndbnd  37818  prdsbnd  37822  heiborlem1  37840  rrnequiv  37864  reheibor  37868  iccbnd  37869  pmapssbaN  39784  2polssN  39939  paddunN  39951  poldmj1N  39952  ispsubcl2N  39971  psubclinN  39972  paddatclN  39973  poml4N  39977  diaglbN  41079  diaintclN  41082  dibglbN  41190  dibintclN  41191  dicssdvh  41210  dihvalrel  41303  dochexmidlem4  41487  infdesc  42641  rmxyelqirrOLD  42909  ttac  43035  hbtlem6  43128  hbt  43129  cnvssb  43585  cnvrcl0  43624  cnvtrrel  43669  relexpaddss  43717  cotrcltrcl  43724  cotrclrcl  43741  frege96d  43748  frege97d  43751  frege109d  43756  frege131d  43763  rfovcnvf1od  44003  isotone2  44048  gneispace  44133  k0004ss1  44150  grumnudlem  44284  uzfissfz  45333  suplesup  45346  ssrexr  45439  limciccioolb  45630  limcicciooub  45646  limcleqr  45653  cnrefiisplem  45838  cncfiooicclem1  45902  ibliccsinexp  45960  iblioosinexp  45962  itgcoscmulx  45978  itgsincmulx  45983  itgsubsticclem  45984  itgiccshift  45989  itgperiod  45990  itgsbtaddcnst  45991  stoweidlem34  46043  stoweidlem59  46068  dirkeritg  46111  dirkercncflem2  46113  fourierdlem20  46136  fourierdlem31  46147  fourierdlem39  46155  fourierdlem42  46158  fourierdlem46  46161  fourierdlem52  46167  fourierdlem53  46168  fourierdlem60  46175  fourierdlem61  46176  fourierdlem62  46177  fourierdlem68  46183  fourierdlem76  46191  fourierdlem85  46200  fourierdlem88  46203  fourierdlem89  46204  fourierdlem90  46205  fourierdlem91  46206  fourierdlem93  46208  fourierdlem94  46209  fourierdlem103  46218  fourierdlem104  46219  fourierdlem111  46226  fouriersw  46240  etransclem46  46289  etransclem48  46291  sge0less  46401  sge0resplit  46415  sge0isum  46436  pimdecfgtioo  46726  pimincfltioo  46727  iccpartipre  47415  bgoldbtbndlem2  47800  setrec1lem4  49534  setrec2fun  49536