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 3889

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 3906

This theorem is referenced by:  difss2  4078  rintn0  5051  eqbrrdva  5824  ssxpb  6138  resssxp  6234  relfld  6239  funssxp  6696  dff2  7051  dff3  7052  fliftf  7270  1stcof  7972  2ndcof  7973  frxp2  8094  frxp3  8101  frrlem13  8248  nnunifi  9201  elfiun  9343  marypha1lem  9346  marypha1  9347  ordtypelem7  9439  tcmin  9660  unwf  9734  rankfu  9801  tcrank  9808  aceq3lem  10042  dfac12lem2  10067  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1lem16  10156  fin23lem26  10247  fin23lem27  10250  fin1a2lem6  10327  itunitc  10343  axdc3lem2  10373  ttukeylem5  10435  fpwwe2lem12  10565  canthwelem  10573  pwfseqlem4  10585  wunex2  10661  wunex3  10664  inar1  10698  inatsk  10701  gruina  10741  suprfinzcl  12643  suprzub  12889  uzsupss  12890  uzwo3  12893  rpnnen1lem4  12930  rpnnen1lem5  12931  supxrre  13279  infxrre  13289  ioodisj  13435  supicclub2  13457  fzssnn  13522  fzossnn0  13645  elfzom1elp1fzo  13687  injresinjlem  13745  uzindi  13944  ssnn0fi  13947  seqcoll  14426  seqcoll2  14427  reltrclfv  14979  relexpdmg  15004  relexpdm  15005  relexprng  15008  relexprn  15009  relexpfld  15011  relexpaddg  15015  limsupval2  15442  limsupgre  15443  limsupbnd2  15445  rlimuni  15512  rlimcld2  15540  rlimno1  15616  isercolllem2  15628  isercoll  15630  summolem2a  15677  summolem2  15678  fsumsers  15690  fsumcvg3  15691  prodmolem2a  15899  prodmolem2  15900  zprod  15902  lcmfnnval  16593  lcmfnncl  16598  prmdvdsbc  16696  4sqlem11  16926  vdwlem8  16959  vdwlem11  16962  ramub2  16985  0ram  16991  0ram2  16992  0ramcl  16994  ramub1lem2  16998  prmgaplem3  17024  prmgaplem4  17025  isohom  17743  funcres2c  17870  resscntz  19308  cntzidss  19315  cntzmhm2  19317  pgpssslw  19589  cntzspan  19819  gsumval3  19882  gsum2d  19947  dprdspan  20004  dprdres  20005  subdrgint  20780  sdrgint  20781  primefld  20782  lssintcl  20959  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  islinds3  21814  fctop  22969  cctop  22971  neitr  23145  ordtbas2  23156  ordtopn1  23159  ordtopn2  23160  lmss  23263  clsconn  23395  2ndcdisj  23421  2ndcomap  23423  ptbasfi  23546  txcmplem2  23607  hausdiag  23610  txkgen  23617  basqtop  23676  alexsubb  24011  alexsubALTlem4  24015  tsmsres  24109  tsmsxplem1  24118  tsmsxp  24120  ustrel  24177  utop3cls  24216  prdsmet  24335  metustrel  24517  icccmplem2  24789  xrge0tsms  24800  cnmptre  24894  icchmeo  24908  bndth  24925  lebnumlem2  24929  cfilresi  25262  causs  25265  bcthlem5  25295  evthicc  25426  ovolficcss  25436  ovolmge0  25444  ovolgelb  25447  ovollb2lem  25455  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliunlem2  25470  ovoliun  25472  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem4  25487  ovolicc2  25489  voliunlem2  25518  voliunlem3  25519  ioombl1lem2  25526  ioombl1lem4  25528  uniioovol  25546  uniiccvol  25547  uniioombllem1  25548  uniioombllem2  25550  uniioombllem3  25552  uniioombllem4  25553  uniioombllem6  25555  dyadmbllem  25566  dyadmbl  25567  volcn  25573  vitalilem4  25578  vitalilem5  25579  cnmbf  25626  i1fmul  25663  itg1addlem4  25666  itg2seq  25709  dvbssntr  25867  dvreslem  25876  dvcjbr  25916  dvferm1  25952  dvferm2  25954  cmvth  25958  dvlip  25960  lhop1lem  25980  lhop2  25982  lhop  25983  dvcnvrelem2  25985  dvcnvre  25986  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumlem2  25994  ftc1a  26004  ftc1lem3  26005  ftc1lem6  26008  itgsubstlem  26015  itgpowd  26017  mdegleb  26029  mdeglt  26030  mdegldg  26031  mdegxrcl  26032  mdegcl  26034  deg1mul3le  26082  ig1pdvds  26145  plyeq0lem  26175  aannenlem2  26295  aalioulem3  26300  taylf  26326  taylthlem2  26339  pserulm  26387  psercn2  26388  psercn  26391  reeff1olem  26411  efcvx  26414  loglesqrt  26725  rlimcnp  26929  xrlimcnp  26932  jensen  26952  wilthlem2  27032  vmadivsumb  27446  pntrsumo1  27528  pntlem3  27572  noseqrdgfn  28298  bdaypw2n0bndlem  28455  perpln2  28779  axcontlem10  29042  usgrexmplef  29328  dfpth2  29797  nmoxr  30837  nmooge0  30838  nmoolb  30842  nmoubi  30843  ubthlem1  30941  shmodi  31461  nmopxr  31937  nmfnxr  31950  nmoplb  31978  nmopub  31979  nmfnlb  31995  nmfnleub  31996  nmopun  32085  branmfn  32176  mdslj1i  32390  hatomistici  32433  xppreima2  32724  fsuppcurry1  32797  fsuppcurry2  32798  fpwrelmap  32806  infxrge0gelb  32839  gsumpart  33124  xrge0tsmsd  33134  pmtrcnel2  33151  cyc3genpm  33213  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  1fldgenq  33383  ssdifidllem  33516  ssmxidllem  33533  mplmulmvr  33683  zarcmplem  34025  metideq  34037  metider  34038  pstmfval  34040  esumgect  34234  esum2d  34237  sigaclci  34276  insiga  34281  omssubadd  34444  eulerpartlemgs2  34524  ballotlemsima  34660  signsply0  34695  iblidicc  34736  fsum2dsub  34751  reprsuc  34759  reprgt  34765  bnj1145  35135  bnj1137  35137  bnj1136  35139  resconn  35428  cvmliftlem8  35474  cvmlift3lem6  35506  mclsssvlem  35744  mclsind  35752  mclsppslem  35765  ivthALT  36517  neibastop1  36541  topjoin  36547  dfttc2g  36688  bj-imdirco  37504  ptrecube  37941  poimirlem6  37947  poimirlem15  37956  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anclem3  38016  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirclem2  38030  areacirclem3  38031  areacirclem4  38032  totbndbnd  38110  prdsbnd  38114  heiborlem1  38132  rrnequiv  38156  reheibor  38160  iccbnd  38161  pmapssbaN  40206  2polssN  40361  paddunN  40373  poldmj1N  40374  ispsubcl2N  40393  psubclinN  40394  paddatclN  40395  poml4N  40399  diaglbN  41501  diaintclN  41504  dibglbN  41612  dibintclN  41613  dicssdvh  41632  dihvalrel  41725  dochexmidlem4  41909  infdesc  43076  ttac  43464  hbtlem6  43557  hbt  43558  cnvssb  44013  cnvrcl0  44052  cnvtrrel  44097  relexpaddss  44145  cotrcltrcl  44152  cotrclrcl  44169  frege96d  44176  frege97d  44179  frege109d  44184  frege131d  44191  rfovcnvf1od  44431  isotone2  44476  gneispace  44561  k0004ss1  44578  grumnudlem  44712  uzfissfz  45756  suplesup  45769  ssrexr  45860  limciccioolb  46051  limcicciooub  46065  limcleqr  46072  cnrefiisplem  46257  cncfiooicclem1  46321  ibliccsinexp  46379  iblioosinexp  46381  itgcoscmulx  46397  itgsincmulx  46402  itgsubsticclem  46403  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem34  46462  stoweidlem59  46487  dirkeritg  46530  dirkercncflem2  46532  fourierdlem20  46555  fourierdlem31  46566  fourierdlem39  46574  fourierdlem42  46577  fourierdlem46  46580  fourierdlem52  46586  fourierdlem53  46587  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem68  46602  fourierdlem76  46610  fourierdlem85  46619  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem93  46627  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fouriersw  46659  etransclem46  46708  etransclem48  46710  sge0less  46820  sge0resplit  46834  sge0isum  46855  hoicvr  46976  pimdecfgtioo  47145  pimincfltioo  47146  iccpartipre  47881  bgoldbtbndlem2  48282  setrec1lem4  50165  setrec2fun  50167