Theorem sstrdi 3934

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

Syntax hints:   → wi 4   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  difss2  4069  rintn0  5039  eqbrrdva  5781  ssxpb  6082  resssxp  6177  relfld  6182  funssxp  6638  dff2  6984  dff3  6985  fliftf  7195  1stcof  7870  2ndcof  7871  frrlem13  8123  nnunifi  9074  elfiun  9198  marypha1lem  9201  marypha1  9202  ordtypelem7  9292  tcmin  9508  unwf  9577  rankfu  9644  tcrank  9651  aceq3lem  9885  dfac12lem2  9909  ackbij1lem9  9993  ackbij1lem10  9994  ackbij1lem16  10000  fin23lem26  10090  fin23lem27  10093  fin1a2lem6  10170  itunitc  10186  axdc3lem2  10216  ttukeylem5  10278  fpwwe2lem12  10407  canthwelem  10415  pwfseqlem4  10427  wunex2  10503  wunex3  10506  inar1  10540  inatsk  10543  gruina  10583  suprfinzcl  12445  suprzub  12688  uzsupss  12689  uzwo3  12692  rpnnen1lem4  12729  rpnnen1lem5  12730  supxrre  13070  infxrre  13079  ioodisj  13223  supicclub2  13245  fzssnn  13309  fzossnn0  13427  elfzom1elp1fzo  13463  injresinjlem  13516  uzindi  13711  ssnn0fi  13714  seqcoll  14187  seqcoll2  14188  reltrclfv  14737  relexpdmg  14762  relexpdm  14763  relexprng  14766  relexprn  14767  relexpfld  14769  relexpaddg  14773  limsupval2  15198  limsupgre  15199  limsupbnd2  15201  rlimuni  15268  rlimcld2  15296  rlimno1  15374  isercolllem2  15386  isercoll  15388  summolem2a  15436  summolem2  15437  fsumsers  15449  fsumcvg3  15450  prodmolem2a  15653  prodmolem2  15654  zprod  15656  lcmfnnval  16338  lcmfnncl  16343  4sqlem11  16665  vdwlem8  16698  vdwlem11  16701  ramub2  16724  0ram  16730  0ram2  16731  0ramcl  16733  ramub1lem2  16737  prmgaplem3  16763  prmgaplem4  16764  isohom  17497  funcres2c  17626  resscntz  18947  cntzidss  18953  cntzmhm2  18955  pgpssslw  19228  cntzspan  19454  gsumval3  19517  gsum2d  19582  dprdspan  19639  dprdres  19640  subdrgint  20080  sdrgint  20081  primefld  20082  lssintcl  20235  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  islinds3  21050  fctop  22163  cctop  22165  neitr  22340  ordtbas2  22351  ordtopn1  22354  ordtopn2  22355  lmss  22458  clsconn  22590  2ndcdisj  22616  2ndcomap  22618  ptbasfi  22741  txcmplem2  22802  hausdiag  22805  txkgen  22812  basqtop  22871  alexsubb  23206  alexsubALTlem4  23210  tsmsres  23304  tsmsxplem1  23313  tsmsxp  23315  ustrel  23372  utop3cls  23412  prdsmet  23532  metustrel  23717  icccmplem2  23995  xrge0tsms  24006  cnmptre  24099  icchmeo  24113  bndth  24130  lebnumlem2  24134  cfilresi  24468  causs  24471  bcthlem5  24501  evthicc  24632  ovolficcss  24642  ovolmge0  24650  ovolgelb  24653  ovollb2lem  24661  ovollb2  24662  ovolunlem1a  24669  ovolunlem1  24670  ovoliunlem1  24675  ovoliunlem2  24676  ovoliun  24678  ovolscalem1  24686  ovolicc1  24689  ovolicc2lem4  24693  ovolicc2  24695  voliunlem2  24724  voliunlem3  24725  ioombl1lem2  24732  ioombl1lem4  24734  uniioovol  24752  uniiccvol  24753  uniioombllem1  24754  uniioombllem2  24756  uniioombllem3  24758  uniioombllem4  24759  uniioombllem6  24761  dyadmbllem  24772  dyadmbl  24773  volcn  24779  vitalilem4  24784  vitalilem5  24785  cnmbf  24832  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  itg2seq  24916  dvbssntr  25073  dvreslem  25082  dvcjbr  25122  dvferm1  25158  dvferm2  25160  cmvth  25164  dvlip  25166  lhop1lem  25186  lhop2  25188  lhop  25189  dvcnvrelem2  25191  dvcnvre  25192  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvfsumlem2  25200  ftc1a  25210  ftc1lem3  25211  ftc1lem6  25214  itgsubstlem  25221  itgpowd  25223  mdegleb  25238  mdeglt  25239  mdegldg  25240  mdegxrcl  25241  mdegcl  25243  deg1mul3le  25290  ig1pdvds  25350  plyeq0lem  25380  aannenlem2  25498  aalioulem3  25503  taylf  25529  taylthlem2  25542  pserulm  25590  psercn2  25591  psercn  25594  reeff1olem  25614  efcvx  25617  loglesqrt  25920  rlimcnp  26124  xrlimcnp  26127  jensen  26147  wilthlem2  26227  vmadivsumb  26640  pntrsumo1  26722  pntlem3  26766  perpln2  27081  axcontlem10  27350  usgrexmplef  27635  nmoxr  29137  nmooge0  29138  nmoolb  29142  nmoubi  29143  ubthlem1  29241  shmodi  29761  nmopxr  30237  nmfnxr  30250  nmoplb  30278  nmopub  30279  nmfnlb  30295  nmfnleub  30296  nmopun  30385  branmfn  30476  mdslj1i  30690  hatomistici  30733  xppreima2  30997  fsuppcurry1  31069  fsuppcurry2  31070  fpwrelmap  31077  infxrge0gelb  31098  prmdvdsbc  31139  gsumpart  31324  xrge0tsmsd  31326  pmtrcnel2  31368  cyc3genpm  31428  ssmxidllem  31650  zarcmplem  31840  metideq  31852  metider  31853  pstmfval  31855  esumgect  32067  esum2d  32070  sigaclci  32109  insiga  32114  omssubadd  32276  eulerpartlemgs2  32356  ballotlemsima  32491  signsply0  32539  iblidicc  32581  fsum2dsub  32596  reprsuc  32604  reprgt  32610  bnj1145  32982  bnj1137  32984  bnj1136  32986  resconn  33217  cvmliftlem8  33263  cvmlift3lem6  33295  mclsssvlem  33533  mclsind  33541  mclsppslem  33554  frxp2  33800  frxp3  33806  ivthALT  34533  neibastop1  34557  topjoin  34563  bj-imdirco  35370  ptrecube  35786  poimirlem6  35792  poimirlem15  35801  heicant  35821  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2gt0cn  35841  ftc1cnnc  35858  ftc1anclem3  35861  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirclem2  35875  areacirclem3  35876  areacirclem4  35877  totbndbnd  35956  prdsbnd  35960  heiborlem1  35978  rrnequiv  36002  reheibor  36006  iccbnd  36007  pmapssbaN  37781  2polssN  37936  paddunN  37948  poldmj1N  37949  ispsubcl2N  37968  psubclinN  37969  paddatclN  37970  poml4N  37974  diaglbN  39076  diaintclN  39079  dibglbN  39187  dibintclN  39188  dicssdvh  39207  dihvalrel  39300  dochexmidlem4  39484  infdesc  40487  rmxyelqirr  40739  ttac  40865  hbtlem6  40961  hbt  40962  cnvssb  41201  cnvrcl0  41240  cnvtrrel  41285  relexpaddss  41333  cotrcltrcl  41340  cotrclrcl  41357  frege96d  41364  frege97d  41367  frege109d  41372  frege131d  41379  rfovcnvf1od  41619  isotone2  41666  gneispace  41751  k0004ss1  41768  grumnudlem  41910  uzfissfz  42872  suplesup  42885  ssrexr  42979  limciccioolb  43169  limcicciooub  43185  limcleqr  43192  cnrefiisplem  43377  cncfiooicclem1  43441  ibliccsinexp  43499  iblioosinexp  43501  itgcoscmulx  43517  itgsincmulx  43522  itgsubsticclem  43523  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem34  43582  stoweidlem59  43607  dirkeritg  43650  dirkercncflem2  43652  fourierdlem20  43675  fourierdlem31  43686  fourierdlem39  43694  fourierdlem42  43697  fourierdlem46  43700  fourierdlem52  43706  fourierdlem53  43707  fourierdlem60  43714  fourierdlem61  43715  fourierdlem62  43716  fourierdlem68  43722  fourierdlem76  43730  fourierdlem85  43739  fourierdlem88  43742  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem93  43747  fourierdlem94  43748  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fouriersw  43779  etransclem46  43828  etransclem48  43830  sge0less  43937  sge0resplit  43951  sge0isum  43972  pimdecfgtioo  44262  pimincfltioo  44263  iccpartipre  44884  bgoldbtbndlem2  45269  setrec1lem4  46407  setrec2fun  46409