Theorem sstrdi 4021

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

Syntax hints:   → wi 4   ⊆ wss 3976

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

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

This theorem is referenced by:  difss2  4161  rintn0  5132  eqbrrdva  5894  ssxpb  6205  resssxp  6301  relfld  6306  funssxp  6776  dff2  7133  dff3  7134  fliftf  7351  1stcof  8060  2ndcof  8061  frxp2  8185  frxp3  8192  frrlem13  8339  nnunifi  9355  elfiun  9499  marypha1lem  9502  marypha1  9503  ordtypelem7  9593  tcmin  9810  unwf  9879  rankfu  9946  tcrank  9953  aceq3lem  10189  dfac12lem2  10214  ackbij1lem9  10296  ackbij1lem10  10297  ackbij1lem16  10303  fin23lem26  10394  fin23lem27  10397  fin1a2lem6  10474  itunitc  10490  axdc3lem2  10520  ttukeylem5  10582  fpwwe2lem12  10711  canthwelem  10719  pwfseqlem4  10731  wunex2  10807  wunex3  10810  inar1  10844  inatsk  10847  gruina  10887  suprfinzcl  12757  suprzub  13004  uzsupss  13005  uzwo3  13008  rpnnen1lem4  13045  rpnnen1lem5  13046  supxrre  13389  infxrre  13398  ioodisj  13542  supicclub2  13564  fzssnn  13628  fzossnn0  13747  elfzom1elp1fzo  13783  injresinjlem  13837  uzindi  14033  ssnn0fi  14036  seqcoll  14513  seqcoll2  14514  reltrclfv  15066  relexpdmg  15091  relexpdm  15092  relexprng  15095  relexprn  15096  relexpfld  15098  relexpaddg  15102  limsupval2  15526  limsupgre  15527  limsupbnd2  15529  rlimuni  15596  rlimcld2  15624  rlimno1  15702  isercolllem2  15714  isercoll  15716  summolem2a  15763  summolem2  15764  fsumsers  15776  fsumcvg3  15777  prodmolem2a  15982  prodmolem2  15983  zprod  15985  lcmfnnval  16671  lcmfnncl  16676  prmdvdsbc  16773  4sqlem11  17002  vdwlem8  17035  vdwlem11  17038  ramub2  17061  0ram  17067  0ram2  17068  0ramcl  17070  ramub1lem2  17074  prmgaplem3  17100  prmgaplem4  17101  isohom  17837  funcres2c  17968  resscntz  19373  cntzidss  19380  cntzmhm2  19382  pgpssslw  19656  cntzspan  19886  gsumval3  19949  gsum2d  20014  dprdspan  20071  dprdres  20072  subdrgint  20826  sdrgint  20827  primefld  20828  lssintcl  20985  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  islinds3  21877  fctop  23032  cctop  23034  neitr  23209  ordtbas2  23220  ordtopn1  23223  ordtopn2  23224  lmss  23327  clsconn  23459  2ndcdisj  23485  2ndcomap  23487  ptbasfi  23610  txcmplem2  23671  hausdiag  23674  txkgen  23681  basqtop  23740  alexsubb  24075  alexsubALTlem4  24079  tsmsres  24173  tsmsxplem1  24182  tsmsxp  24184  ustrel  24241  utop3cls  24281  prdsmet  24401  metustrel  24586  icccmplem2  24864  xrge0tsms  24875  cnmptre  24973  icchmeo  24990  icchmeoOLD  24991  bndth  25009  lebnumlem2  25013  cfilresi  25348  causs  25351  bcthlem5  25381  evthicc  25513  ovolficcss  25523  ovolmge0  25531  ovolgelb  25534  ovollb2lem  25542  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliunlem2  25557  ovoliun  25559  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem4  25574  ovolicc2  25576  voliunlem2  25605  voliunlem3  25606  ioombl1lem2  25613  ioombl1lem4  25615  uniioovol  25633  uniiccvol  25634  uniioombllem1  25635  uniioombllem2  25637  uniioombllem3  25639  uniioombllem4  25640  uniioombllem6  25642  dyadmbllem  25653  dyadmbl  25654  volcn  25660  vitalilem4  25665  vitalilem5  25666  cnmbf  25713  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  itg2seq  25797  dvbssntr  25955  dvreslem  25964  dvcjbr  26007  dvferm1  26043  dvferm2  26045  cmvth  26049  cmvthOLD  26050  dvlip  26052  lhop1lem  26072  lhop2  26074  lhop  26075  dvcnvrelem2  26077  dvcnvre  26078  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  ftc1a  26098  ftc1lem3  26099  ftc1lem6  26102  itgsubstlem  26109  itgpowd  26111  mdegleb  26123  mdeglt  26124  mdegldg  26125  mdegxrcl  26126  mdegcl  26128  deg1mul3le  26176  ig1pdvds  26239  plyeq0lem  26269  aannenlem2  26389  aalioulem3  26394  taylf  26420  taylthlem2  26434  taylthlem2OLD  26435  pserulm  26483  psercn2  26484  psercn2OLD  26485  psercn  26488  reeff1olem  26508  efcvx  26511  loglesqrt  26822  rlimcnp  27026  xrlimcnp  27029  jensen  27050  wilthlem2  27130  vmadivsumb  27545  pntrsumo1  27627  pntlem3  27671  noseqrdgfn  28330  perpln2  28737  axcontlem10  29006  usgrexmplef  29294  nmoxr  30798  nmooge0  30799  nmoolb  30803  nmoubi  30804  ubthlem1  30902  shmodi  31422  nmopxr  31898  nmfnxr  31911  nmoplb  31939  nmopub  31940  nmfnlb  31956  nmfnleub  31957  nmopun  32046  branmfn  32137  mdslj1i  32351  hatomistici  32394  xppreima2  32669  fsuppcurry1  32739  fsuppcurry2  32740  fpwrelmap  32747  infxrge0gelb  32773  gsumpart  33038  xrge0tsmsd  33041  pmtrcnel2  33083  cyc3genpm  33145  1fldgenq  33289  ssdifidllem  33449  ssmxidllem  33466  zarcmplem  33827  metideq  33839  metider  33840  pstmfval  33842  esumgect  34054  esum2d  34057  sigaclci  34096  insiga  34101  omssubadd  34265  eulerpartlemgs2  34345  ballotlemsima  34480  signsply0  34528  iblidicc  34569  fsum2dsub  34584  reprsuc  34592  reprgt  34598  bnj1145  34969  bnj1137  34971  bnj1136  34973  resconn  35214  cvmliftlem8  35260  cvmlift3lem6  35292  mclsssvlem  35530  mclsind  35538  mclsppslem  35551  ivthALT  36301  neibastop1  36325  topjoin  36331  bj-imdirco  37156  ptrecube  37580  poimirlem6  37586  poimirlem15  37595  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2gt0cn  37635  ftc1cnnc  37652  ftc1anclem3  37655  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirclem2  37669  areacirclem3  37670  areacirclem4  37671  totbndbnd  37749  prdsbnd  37753  heiborlem1  37771  rrnequiv  37795  reheibor  37799  iccbnd  37800  pmapssbaN  39717  2polssN  39872  paddunN  39884  poldmj1N  39885  ispsubcl2N  39904  psubclinN  39905  paddatclN  39906  poml4N  39910  diaglbN  41012  diaintclN  41015  dibglbN  41123  dibintclN  41124  dicssdvh  41143  dihvalrel  41236  dochexmidlem4  41420  infdesc  42598  rmxyelqirrOLD  42867  ttac  42993  hbtlem6  43086  hbt  43087  cnvssb  43548  cnvrcl0  43587  cnvtrrel  43632  relexpaddss  43680  cotrcltrcl  43687  cotrclrcl  43704  frege96d  43711  frege97d  43714  frege109d  43719  frege131d  43726  rfovcnvf1od  43966  isotone2  44011  gneispace  44096  k0004ss1  44113  grumnudlem  44254  uzfissfz  45241  suplesup  45254  ssrexr  45347  limciccioolb  45542  limcicciooub  45558  limcleqr  45565  cnrefiisplem  45750  cncfiooicclem1  45814  ibliccsinexp  45872  iblioosinexp  45874  itgcoscmulx  45890  itgsincmulx  45895  itgsubsticclem  45896  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem34  45955  stoweidlem59  45980  dirkeritg  46023  dirkercncflem2  46025  fourierdlem20  46048  fourierdlem31  46059  fourierdlem39  46067  fourierdlem42  46070  fourierdlem46  46073  fourierdlem52  46079  fourierdlem53  46080  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem68  46095  fourierdlem76  46103  fourierdlem85  46112  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem93  46120  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fouriersw  46152  etransclem46  46201  etransclem48  46203  sge0less  46313  sge0resplit  46327  sge0isum  46348  pimdecfgtioo  46638  pimincfltioo  46639  iccpartipre  47295  bgoldbtbndlem2  47680  setrec1lem4  48782  setrec2fun  48784