Theorem sstrdi 3950

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

Syntax hints:   → wi 4   ⊆ wss 3905

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 3922

This theorem is referenced by:  difss2  4091  rintn0  5061  eqbrrdva  5816  ssxpb  6127  resssxp  6222  relfld  6227  funssxp  6684  dff2  7037  dff3  7038  fliftf  7256  1stcof  7961  2ndcof  7962  frxp2  8084  frxp3  8091  frrlem13  8238  nnunifi  9196  elfiun  9339  marypha1lem  9342  marypha1  9343  ordtypelem7  9435  tcmin  9656  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  10555  canthwelem  10563  pwfseqlem4  10575  wunex2  10651  wunex3  10654  inar1  10688  inatsk  10691  gruina  10731  suprfinzcl  12609  suprzub  12859  uzsupss  12860  uzwo3  12863  rpnnen1lem4  12900  rpnnen1lem5  12901  supxrre  13248  infxrre  13258  ioodisj  13404  supicclub2  13426  fzssnn  13490  fzossnn0  13612  elfzom1elp1fzo  13654  injresinjlem  13709  uzindi  13908  ssnn0fi  13911  seqcoll  14390  seqcoll2  14391  reltrclfv  14943  relexpdmg  14968  relexpdm  14969  relexprng  14972  relexprn  14973  relexpfld  14975  relexpaddg  14979  limsupval2  15406  limsupgre  15407  limsupbnd2  15409  rlimuni  15476  rlimcld2  15504  rlimno1  15580  isercolllem2  15592  isercoll  15594  summolem2a  15641  summolem2  15642  fsumsers  15654  fsumcvg3  15655  prodmolem2a  15860  prodmolem2  15861  zprod  15863  lcmfnnval  16554  lcmfnncl  16559  prmdvdsbc  16656  4sqlem11  16886  vdwlem8  16919  vdwlem11  16922  ramub2  16945  0ram  16951  0ram2  16952  0ramcl  16954  ramub1lem2  16958  prmgaplem3  16984  prmgaplem4  16985  isohom  17702  funcres2c  17829  resscntz  19231  cntzidss  19238  cntzmhm2  19240  pgpssslw  19512  cntzspan  19742  gsumval3  19805  gsum2d  19870  dprdspan  19927  dprdres  19928  subdrgint  20707  sdrgint  20708  primefld  20709  lssintcl  20886  lbsextlem2  21085  lbsextlem3  21086  lbsextlem4  21087  islinds3  21760  fctop  22908  cctop  22910  neitr  23084  ordtbas2  23095  ordtopn1  23098  ordtopn2  23099  lmss  23202  clsconn  23334  2ndcdisj  23360  2ndcomap  23362  ptbasfi  23485  txcmplem2  23546  hausdiag  23549  txkgen  23556  basqtop  23615  alexsubb  23950  alexsubALTlem4  23954  tsmsres  24048  tsmsxplem1  24057  tsmsxp  24059  ustrel  24116  utop3cls  24156  prdsmet  24275  metustrel  24457  icccmplem2  24729  xrge0tsms  24740  cnmptre  24838  icchmeo  24855  icchmeoOLD  24856  bndth  24874  lebnumlem2  24878  cfilresi  25212  causs  25215  bcthlem5  25245  evthicc  25377  ovolficcss  25387  ovolmge0  25395  ovolgelb  25398  ovollb2lem  25406  ovollb2  25407  ovolunlem1a  25414  ovolunlem1  25415  ovoliunlem1  25420  ovoliunlem2  25421  ovoliun  25423  ovolscalem1  25431  ovolicc1  25434  ovolicc2lem4  25438  ovolicc2  25440  voliunlem2  25469  voliunlem3  25470  ioombl1lem2  25477  ioombl1lem4  25479  uniioovol  25497  uniiccvol  25498  uniioombllem1  25499  uniioombllem2  25501  uniioombllem3  25503  uniioombllem4  25504  uniioombllem6  25506  dyadmbllem  25517  dyadmbl  25518  volcn  25524  vitalilem4  25529  vitalilem5  25530  cnmbf  25577  i1fmul  25614  itg1addlem4  25617  itg2seq  25660  dvbssntr  25818  dvreslem  25827  dvcjbr  25870  dvferm1  25906  dvferm2  25908  cmvth  25912  cmvthOLD  25913  dvlip  25915  lhop1lem  25935  lhop2  25937  lhop  25938  dvcnvrelem2  25940  dvcnvre  25941  dvfsumle  25943  dvfsumleOLD  25944  dvfsumge  25945  dvfsumabs  25946  dvfsumlem2  25950  dvfsumlem2OLD  25951  ftc1a  25961  ftc1lem3  25962  ftc1lem6  25965  itgsubstlem  25972  itgpowd  25974  mdegleb  25986  mdeglt  25987  mdegldg  25988  mdegxrcl  25989  mdegcl  25991  deg1mul3le  26039  ig1pdvds  26102  plyeq0lem  26132  aannenlem2  26254  aalioulem3  26259  taylf  26285  taylthlem2  26299  taylthlem2OLD  26300  pserulm  26348  psercn2  26349  psercn2OLD  26350  psercn  26353  reeff1olem  26373  efcvx  26376  loglesqrt  26688  rlimcnp  26892  xrlimcnp  26895  jensen  26916  wilthlem2  26996  vmadivsumb  27411  pntrsumo1  27493  pntlem3  27537  noseqrdgfn  28224  perpln2  28675  axcontlem10  28937  usgrexmplef  29223  dfpth2  29693  nmoxr  30729  nmooge0  30730  nmoolb  30734  nmoubi  30735  ubthlem1  30833  shmodi  31353  nmopxr  31829  nmfnxr  31842  nmoplb  31870  nmopub  31871  nmfnlb  31887  nmfnleub  31888  nmopun  31977  branmfn  32068  mdslj1i  32282  hatomistici  32325  xppreima2  32613  fsuppcurry1  32687  fsuppcurry2  32688  fpwrelmap  32695  infxrge0gelb  32728  gsumpart  33029  xrge0tsmsd  33034  pmtrcnel2  33051  cyc3genpm  33113  elrgspnsubrunlem1  33206  elrgspnsubrunlem2  33207  1fldgenq  33280  ssdifidllem  33412  ssmxidllem  33429  zarcmplem  33867  metideq  33879  metider  33880  pstmfval  33882  esumgect  34076  esum2d  34079  sigaclci  34118  insiga  34123  omssubadd  34287  eulerpartlemgs2  34367  ballotlemsima  34503  signsply0  34538  iblidicc  34579  fsum2dsub  34594  reprsuc  34602  reprgt  34608  bnj1145  34979  bnj1137  34981  bnj1136  34983  resconn  35238  cvmliftlem8  35284  cvmlift3lem6  35316  mclsssvlem  35554  mclsind  35562  mclsppslem  35575  ivthALT  36328  neibastop1  36352  topjoin  36358  bj-imdirco  37183  ptrecube  37619  poimirlem6  37625  poimirlem15  37634  heicant  37654  mblfinlem2  37657  mblfinlem3  37658  mblfinlem4  37659  ismblfin  37660  itg2gt0cn  37674  ftc1cnnc  37691  ftc1anclem3  37694  ftc1anclem7  37698  ftc1anclem8  37699  ftc1anc  37700  areacirclem2  37708  areacirclem3  37709  areacirclem4  37710  totbndbnd  37788  prdsbnd  37792  heiborlem1  37810  rrnequiv  37834  reheibor  37838  iccbnd  37839  pmapssbaN  39759  2polssN  39914  paddunN  39926  poldmj1N  39927  ispsubcl2N  39946  psubclinN  39947  paddatclN  39948  poml4N  39952  diaglbN  41054  diaintclN  41057  dibglbN  41165  dibintclN  41166  dicssdvh  41185  dihvalrel  41278  dochexmidlem4  41462  infdesc  42636  ttac  43029  hbtlem6  43122  hbt  43123  cnvssb  43579  cnvrcl0  43618  cnvtrrel  43663  relexpaddss  43711  cotrcltrcl  43718  cotrclrcl  43735  frege96d  43742  frege97d  43745  frege109d  43750  frege131d  43757  rfovcnvf1od  43997  isotone2  44042  gneispace  44127  k0004ss1  44144  grumnudlem  44278  uzfissfz  45326  suplesup  45339  ssrexr  45431  limciccioolb  45622  limcicciooub  45638  limcleqr  45645  cnrefiisplem  45830  cncfiooicclem1  45894  ibliccsinexp  45952  iblioosinexp  45954  itgcoscmulx  45970  itgsincmulx  45975  itgsubsticclem  45976  itgiccshift  45981  itgperiod  45982  itgsbtaddcnst  45983  stoweidlem34  46035  stoweidlem59  46060  dirkeritg  46103  dirkercncflem2  46105  fourierdlem20  46128  fourierdlem31  46139  fourierdlem39  46147  fourierdlem42  46150  fourierdlem46  46153  fourierdlem52  46159  fourierdlem53  46160  fourierdlem60  46167  fourierdlem61  46168  fourierdlem62  46169  fourierdlem68  46175  fourierdlem76  46183  fourierdlem85  46192  fourierdlem88  46195  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fourierdlem93  46200  fourierdlem94  46201  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  fouriersw  46232  etransclem46  46281  etransclem48  46283  sge0less  46393  sge0resplit  46407  sge0isum  46428  pimdecfgtioo  46718  pimincfltioo  46719  iccpartipre  47425  bgoldbtbndlem2  47810  setrec1lem4  49695  setrec2fun  49697