Theorem sstrdi 3956

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

Syntax hints:   → wi 4   ⊆ wss 3911

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 3928

This theorem is referenced by:  difss2  4097  rintn0  5068  eqbrrdva  5823  ssxpb  6135  resssxp  6231  relfld  6236  funssxp  6698  dff2  7053  dff3  7054  fliftf  7272  1stcof  7977  2ndcof  7978  frxp2  8100  frxp3  8107  frrlem13  8254  nnunifi  9214  elfiun  9357  marypha1lem  9360  marypha1  9361  ordtypelem7  9453  tcmin  9670  unwf  9739  rankfu  9806  tcrank  9813  aceq3lem  10049  dfac12lem2  10074  ackbij1lem9  10156  ackbij1lem10  10157  ackbij1lem16  10163  fin23lem26  10254  fin23lem27  10257  fin1a2lem6  10334  itunitc  10350  axdc3lem2  10380  ttukeylem5  10442  fpwwe2lem12  10571  canthwelem  10579  pwfseqlem4  10591  wunex2  10667  wunex3  10670  inar1  10704  inatsk  10707  gruina  10747  suprfinzcl  12624  suprzub  12874  uzsupss  12875  uzwo3  12878  rpnnen1lem4  12915  rpnnen1lem5  12916  supxrre  13263  infxrre  13273  ioodisj  13419  supicclub2  13441  fzssnn  13505  fzossnn0  13627  elfzom1elp1fzo  13669  injresinjlem  13724  uzindi  13923  ssnn0fi  13926  seqcoll  14405  seqcoll2  14406  reltrclfv  14959  relexpdmg  14984  relexpdm  14985  relexprng  14988  relexprn  14989  relexpfld  14991  relexpaddg  14995  limsupval2  15422  limsupgre  15423  limsupbnd2  15425  rlimuni  15492  rlimcld2  15520  rlimno1  15596  isercolllem2  15608  isercoll  15610  summolem2a  15657  summolem2  15658  fsumsers  15670  fsumcvg3  15671  prodmolem2a  15876  prodmolem2  15877  zprod  15879  lcmfnnval  16570  lcmfnncl  16575  prmdvdsbc  16672  4sqlem11  16902  vdwlem8  16935  vdwlem11  16938  ramub2  16961  0ram  16967  0ram2  16968  0ramcl  16970  ramub1lem2  16974  prmgaplem3  17000  prmgaplem4  17001  isohom  17714  funcres2c  17841  resscntz  19241  cntzidss  19248  cntzmhm2  19250  pgpssslw  19520  cntzspan  19750  gsumval3  19813  gsum2d  19878  dprdspan  19935  dprdres  19936  subdrgint  20688  sdrgint  20689  primefld  20690  lssintcl  20846  lbsextlem2  21045  lbsextlem3  21046  lbsextlem4  21047  islinds3  21719  fctop  22867  cctop  22869  neitr  23043  ordtbas2  23054  ordtopn1  23057  ordtopn2  23058  lmss  23161  clsconn  23293  2ndcdisj  23319  2ndcomap  23321  ptbasfi  23444  txcmplem2  23505  hausdiag  23508  txkgen  23515  basqtop  23574  alexsubb  23909  alexsubALTlem4  23913  tsmsres  24007  tsmsxplem1  24016  tsmsxp  24018  ustrel  24075  utop3cls  24115  prdsmet  24234  metustrel  24416  icccmplem2  24688  xrge0tsms  24699  cnmptre  24797  icchmeo  24814  icchmeoOLD  24815  bndth  24833  lebnumlem2  24837  cfilresi  25171  causs  25174  bcthlem5  25204  evthicc  25336  ovolficcss  25346  ovolmge0  25354  ovolgelb  25357  ovollb2lem  25365  ovollb2  25366  ovolunlem1a  25373  ovolunlem1  25374  ovoliunlem1  25379  ovoliunlem2  25380  ovoliun  25382  ovolscalem1  25390  ovolicc1  25393  ovolicc2lem4  25397  ovolicc2  25399  voliunlem2  25428  voliunlem3  25429  ioombl1lem2  25436  ioombl1lem4  25438  uniioovol  25456  uniiccvol  25457  uniioombllem1  25458  uniioombllem2  25460  uniioombllem3  25462  uniioombllem4  25463  uniioombllem6  25465  dyadmbllem  25476  dyadmbl  25477  volcn  25483  vitalilem4  25488  vitalilem5  25489  cnmbf  25536  i1fmul  25573  itg1addlem4  25576  itg2seq  25619  dvbssntr  25777  dvreslem  25786  dvcjbr  25829  dvferm1  25865  dvferm2  25867  cmvth  25871  cmvthOLD  25872  dvlip  25874  lhop1lem  25894  lhop2  25896  lhop  25897  dvcnvrelem2  25899  dvcnvre  25900  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  ftc1a  25920  ftc1lem3  25921  ftc1lem6  25924  itgsubstlem  25931  itgpowd  25933  mdegleb  25945  mdeglt  25946  mdegldg  25947  mdegxrcl  25948  mdegcl  25950  deg1mul3le  25998  ig1pdvds  26061  plyeq0lem  26091  aannenlem2  26213  aalioulem3  26218  taylf  26244  taylthlem2  26258  taylthlem2OLD  26259  pserulm  26307  psercn2  26308  psercn2OLD  26309  psercn  26312  reeff1olem  26332  efcvx  26335  loglesqrt  26647  rlimcnp  26851  xrlimcnp  26854  jensen  26875  wilthlem2  26955  vmadivsumb  27370  pntrsumo1  27452  pntlem3  27496  noseqrdgfn  28176  perpln2  28614  axcontlem10  28876  usgrexmplef  29162  dfpth2  29632  nmoxr  30668  nmooge0  30669  nmoolb  30673  nmoubi  30674  ubthlem1  30772  shmodi  31292  nmopxr  31768  nmfnxr  31781  nmoplb  31809  nmopub  31810  nmfnlb  31826  nmfnleub  31827  nmopun  31916  branmfn  32007  mdslj1i  32221  hatomistici  32264  xppreima2  32548  fsuppcurry1  32621  fsuppcurry2  32622  fpwrelmap  32629  infxrge0gelb  32662  gsumpart  32970  xrge0tsmsd  32975  pmtrcnel2  33020  cyc3genpm  33082  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  1fldgenq  33245  ssdifidllem  33400  ssmxidllem  33417  zarcmplem  33844  metideq  33856  metider  33857  pstmfval  33859  esumgect  34053  esum2d  34056  sigaclci  34095  insiga  34100  omssubadd  34264  eulerpartlemgs2  34344  ballotlemsima  34480  signsply0  34515  iblidicc  34556  fsum2dsub  34571  reprsuc  34579  reprgt  34585  bnj1145  34956  bnj1137  34958  bnj1136  34960  resconn  35206  cvmliftlem8  35252  cvmlift3lem6  35284  mclsssvlem  35522  mclsind  35530  mclsppslem  35543  ivthALT  36296  neibastop1  36320  topjoin  36326  bj-imdirco  37151  ptrecube  37587  poimirlem6  37593  poimirlem15  37602  heicant  37622  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  itg2gt0cn  37642  ftc1cnnc  37659  ftc1anclem3  37662  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  areacirclem2  37676  areacirclem3  37677  areacirclem4  37678  totbndbnd  37756  prdsbnd  37760  heiborlem1  37778  rrnequiv  37802  reheibor  37806  iccbnd  37807  pmapssbaN  39727  2polssN  39882  paddunN  39894  poldmj1N  39895  ispsubcl2N  39914  psubclinN  39915  paddatclN  39916  poml4N  39920  diaglbN  41022  diaintclN  41025  dibglbN  41133  dibintclN  41134  dicssdvh  41153  dihvalrel  41246  dochexmidlem4  41430  infdesc  42604  rmxyelqirrOLD  42872  ttac  42998  hbtlem6  43091  hbt  43092  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  44247  uzfissfz  45295  suplesup  45308  ssrexr  45401  limciccioolb  45592  limcicciooub  45608  limcleqr  45615  cnrefiisplem  45800  cncfiooicclem1  45864  ibliccsinexp  45922  iblioosinexp  45924  itgcoscmulx  45940  itgsincmulx  45945  itgsubsticclem  45946  itgiccshift  45951  itgperiod  45952  itgsbtaddcnst  45953  stoweidlem34  46005  stoweidlem59  46030  dirkeritg  46073  dirkercncflem2  46075  fourierdlem20  46098  fourierdlem31  46109  fourierdlem39  46117  fourierdlem42  46120  fourierdlem46  46123  fourierdlem52  46129  fourierdlem53  46130  fourierdlem60  46137  fourierdlem61  46138  fourierdlem62  46139  fourierdlem68  46145  fourierdlem76  46153  fourierdlem85  46162  fourierdlem88  46165  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem93  46170  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fouriersw  46202  etransclem46  46251  etransclem48  46253  sge0less  46363  sge0resplit  46377  sge0isum  46398  pimdecfgtioo  46688  pimincfltioo  46689  iccpartipre  47395  bgoldbtbndlem2  47780  setrec1lem4  49652  setrec2fun  49654