Theorem sstrdi 3935

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

Syntax hints:   → wi 4   ⊆ wss 3890

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

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

This theorem is referenced by:  difss2  4079  rintn0  5052  eqbrrdva  5818  ssxpb  6132  resssxp  6228  relfld  6233  funssxp  6690  dff2  7045  dff3  7046  fliftf  7263  1stcof  7965  2ndcof  7966  frxp2  8087  frxp3  8094  frrlem13  8241  nnunifi  9194  elfiun  9336  marypha1lem  9339  marypha1  9340  ordtypelem7  9432  tcmin  9651  unwf  9725  rankfu  9792  tcrank  9799  aceq3lem  10033  dfac12lem2  10058  ackbij1lem9  10140  ackbij1lem10  10141  ackbij1lem16  10147  fin23lem26  10238  fin23lem27  10241  fin1a2lem6  10318  itunitc  10334  axdc3lem2  10364  ttukeylem5  10426  fpwwe2lem12  10556  canthwelem  10564  pwfseqlem4  10576  wunex2  10652  wunex3  10655  inar1  10689  inatsk  10692  gruina  10732  suprfinzcl  12634  suprzub  12880  uzsupss  12881  uzwo3  12884  rpnnen1lem4  12921  rpnnen1lem5  12922  supxrre  13270  infxrre  13280  ioodisj  13426  supicclub2  13448  fzssnn  13513  fzossnn0  13636  elfzom1elp1fzo  13678  injresinjlem  13736  uzindi  13935  ssnn0fi  13938  seqcoll  14417  seqcoll2  14418  reltrclfv  14970  relexpdmg  14995  relexpdm  14996  relexprng  14999  relexprn  15000  relexpfld  15002  relexpaddg  15006  limsupval2  15433  limsupgre  15434  limsupbnd2  15436  rlimuni  15503  rlimcld2  15531  rlimno1  15607  isercolllem2  15619  isercoll  15621  summolem2a  15668  summolem2  15669  fsumsers  15681  fsumcvg3  15682  prodmolem2a  15890  prodmolem2  15891  zprod  15893  lcmfnnval  16584  lcmfnncl  16589  prmdvdsbc  16687  4sqlem11  16917  vdwlem8  16950  vdwlem11  16953  ramub2  16976  0ram  16982  0ram2  16983  0ramcl  16985  ramub1lem2  16989  prmgaplem3  17015  prmgaplem4  17016  isohom  17734  funcres2c  17861  resscntz  19299  cntzidss  19306  cntzmhm2  19308  pgpssslw  19580  cntzspan  19810  gsumval3  19873  gsum2d  19938  dprdspan  19995  dprdres  19996  subdrgint  20771  sdrgint  20772  primefld  20773  lssintcl  20950  lbsextlem2  21149  lbsextlem3  21150  lbsextlem4  21151  islinds3  21824  fctop  22979  cctop  22981  neitr  23155  ordtbas2  23166  ordtopn1  23169  ordtopn2  23170  lmss  23273  clsconn  23405  2ndcdisj  23431  2ndcomap  23433  ptbasfi  23556  txcmplem2  23617  hausdiag  23620  txkgen  23627  basqtop  23686  alexsubb  24021  alexsubALTlem4  24025  tsmsres  24119  tsmsxplem1  24128  tsmsxp  24130  ustrel  24187  utop3cls  24226  prdsmet  24345  metustrel  24527  icccmplem2  24799  xrge0tsms  24810  cnmptre  24904  icchmeo  24918  bndth  24935  lebnumlem2  24939  cfilresi  25272  causs  25275  bcthlem5  25305  evthicc  25436  ovolficcss  25446  ovolmge0  25454  ovolgelb  25457  ovollb2lem  25465  ovollb2  25466  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliunlem2  25480  ovoliun  25482  ovolscalem1  25490  ovolicc1  25493  ovolicc2lem4  25497  ovolicc2  25499  voliunlem2  25528  voliunlem3  25529  ioombl1lem2  25536  ioombl1lem4  25538  uniioovol  25556  uniiccvol  25557  uniioombllem1  25558  uniioombllem2  25560  uniioombllem3  25562  uniioombllem4  25563  uniioombllem6  25565  dyadmbllem  25576  dyadmbl  25577  volcn  25583  vitalilem4  25588  vitalilem5  25589  cnmbf  25636  i1fmul  25673  itg1addlem4  25676  itg2seq  25719  dvbssntr  25877  dvreslem  25886  dvcjbr  25926  dvferm1  25962  dvferm2  25964  cmvth  25968  dvlip  25970  lhop1lem  25990  lhop2  25992  lhop  25993  dvcnvrelem2  25995  dvcnvre  25996  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  dvfsumlem2  26004  ftc1a  26014  ftc1lem3  26015  ftc1lem6  26018  itgsubstlem  26025  itgpowd  26027  mdegleb  26039  mdeglt  26040  mdegldg  26041  mdegxrcl  26042  mdegcl  26044  deg1mul3le  26092  ig1pdvds  26155  plyeq0lem  26185  aannenlem2  26306  aalioulem3  26311  taylf  26337  taylthlem2  26351  taylthlem2OLD  26352  pserulm  26400  psercn2  26401  psercn  26404  reeff1olem  26424  efcvx  26427  loglesqrt  26738  rlimcnp  26942  xrlimcnp  26945  jensen  26966  wilthlem2  27046  vmadivsumb  27460  pntrsumo1  27542  pntlem3  27586  noseqrdgfn  28312  bdaypw2n0bndlem  28469  perpln2  28793  axcontlem10  29056  usgrexmplef  29342  dfpth2  29812  nmoxr  30852  nmooge0  30853  nmoolb  30857  nmoubi  30858  ubthlem1  30956  shmodi  31476  nmopxr  31952  nmfnxr  31965  nmoplb  31993  nmopub  31994  nmfnlb  32010  nmfnleub  32011  nmopun  32100  branmfn  32191  mdslj1i  32405  hatomistici  32448  xppreima2  32739  fsuppcurry1  32812  fsuppcurry2  32813  fpwrelmap  32821  infxrge0gelb  32854  gsumpart  33139  xrge0tsmsd  33149  pmtrcnel2  33166  cyc3genpm  33228  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  1fldgenq  33398  ssdifidllem  33531  ssmxidllem  33548  mplmulmvr  33698  zarcmplem  34041  metideq  34053  metider  34054  pstmfval  34056  esumgect  34250  esum2d  34253  sigaclci  34292  insiga  34297  omssubadd  34460  eulerpartlemgs2  34540  ballotlemsima  34676  signsply0  34711  iblidicc  34752  fsum2dsub  34767  reprsuc  34775  reprgt  34781  bnj1145  35151  bnj1137  35153  bnj1136  35155  resconn  35444  cvmliftlem8  35490  cvmlift3lem6  35522  mclsssvlem  35760  mclsind  35768  mclsppslem  35781  ivthALT  36533  neibastop1  36557  topjoin  36563  dfttc2g  36704  bj-imdirco  37520  ptrecube  37955  poimirlem6  37961  poimirlem15  37970  heicant  37990  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  itg2gt0cn  38010  ftc1cnnc  38027  ftc1anclem3  38030  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  areacirclem2  38044  areacirclem3  38045  areacirclem4  38046  totbndbnd  38124  prdsbnd  38128  heiborlem1  38146  rrnequiv  38170  reheibor  38174  iccbnd  38175  pmapssbaN  40220  2polssN  40375  paddunN  40387  poldmj1N  40388  ispsubcl2N  40407  psubclinN  40408  paddatclN  40409  poml4N  40413  diaglbN  41515  diaintclN  41518  dibglbN  41626  dibintclN  41627  dicssdvh  41646  dihvalrel  41739  dochexmidlem4  41923  infdesc  43090  ttac  43482  hbtlem6  43575  hbt  43576  cnvssb  44031  cnvrcl0  44070  cnvtrrel  44115  relexpaddss  44163  cotrcltrcl  44170  cotrclrcl  44187  frege96d  44194  frege97d  44197  frege109d  44202  frege131d  44209  rfovcnvf1od  44449  isotone2  44494  gneispace  44579  k0004ss1  44596  grumnudlem  44730  uzfissfz  45774  suplesup  45787  ssrexr  45878  limciccioolb  46069  limcicciooub  46083  limcleqr  46090  cnrefiisplem  46275  cncfiooicclem1  46339  ibliccsinexp  46397  iblioosinexp  46399  itgcoscmulx  46415  itgsincmulx  46420  itgsubsticclem  46421  itgiccshift  46426  itgperiod  46427  itgsbtaddcnst  46428  stoweidlem34  46480  stoweidlem59  46505  dirkeritg  46548  dirkercncflem2  46550  fourierdlem20  46573  fourierdlem31  46584  fourierdlem39  46592  fourierdlem42  46595  fourierdlem46  46598  fourierdlem52  46604  fourierdlem53  46605  fourierdlem60  46612  fourierdlem61  46613  fourierdlem62  46614  fourierdlem68  46620  fourierdlem76  46628  fourierdlem85  46637  fourierdlem88  46640  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem93  46645  fourierdlem94  46646  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fouriersw  46677  etransclem46  46726  etransclem48  46728  sge0less  46838  sge0resplit  46852  sge0isum  46873  hoicvr  46994  pimdecfgtioo  47163  pimincfltioo  47164  iccpartipre  47893  bgoldbtbndlem2  48294  setrec1lem4  50177  setrec2fun  50179