Theorem sstrdi 3948

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

Syntax hints:   → wi 4   ⊆ wss 3903

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 3920

This theorem is referenced by:  difss2  4092  rintn0  5066  eqbrrdva  5826  ssxpb  6140  resssxp  6236  relfld  6241  funssxp  6698  dff2  7053  dff3  7054  fliftf  7271  1stcof  7973  2ndcof  7974  frxp2  8096  frxp3  8103  frrlem13  8250  nnunifi  9203  elfiun  9345  marypha1lem  9348  marypha1  9349  ordtypelem7  9441  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  12618  suprzub  12864  uzsupss  12865  uzwo3  12868  rpnnen1lem4  12905  rpnnen1lem5  12906  supxrre  13254  infxrre  13264  ioodisj  13410  supicclub2  13432  fzssnn  13496  fzossnn0  13618  elfzom1elp1fzo  13660  injresinjlem  13718  uzindi  13917  ssnn0fi  13920  seqcoll  14399  seqcoll2  14400  reltrclfv  14952  relexpdmg  14977  relexpdm  14978  relexprng  14981  relexprn  14982  relexpfld  14984  relexpaddg  14988  limsupval2  15415  limsupgre  15416  limsupbnd2  15418  rlimuni  15485  rlimcld2  15513  rlimno1  15589  isercolllem2  15601  isercoll  15603  summolem2a  15650  summolem2  15651  fsumsers  15663  fsumcvg3  15664  prodmolem2a  15869  prodmolem2  15870  zprod  15872  lcmfnnval  16563  lcmfnncl  16568  prmdvdsbc  16665  4sqlem11  16895  vdwlem8  16928  vdwlem11  16931  ramub2  16954  0ram  16960  0ram2  16961  0ramcl  16963  ramub1lem2  16967  prmgaplem3  16993  prmgaplem4  16994  isohom  17712  funcres2c  17839  resscntz  19274  cntzidss  19281  cntzmhm2  19283  pgpssslw  19555  cntzspan  19785  gsumval3  19848  gsum2d  19913  dprdspan  19970  dprdres  19971  subdrgint  20748  sdrgint  20749  primefld  20750  lssintcl  20927  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  islinds3  21801  fctop  22960  cctop  22962  neitr  23136  ordtbas2  23147  ordtopn1  23150  ordtopn2  23151  lmss  23254  clsconn  23386  2ndcdisj  23412  2ndcomap  23414  ptbasfi  23537  txcmplem2  23598  hausdiag  23601  txkgen  23608  basqtop  23667  alexsubb  24002  alexsubALTlem4  24006  tsmsres  24100  tsmsxplem1  24109  tsmsxp  24111  ustrel  24168  utop3cls  24207  prdsmet  24326  metustrel  24508  icccmplem2  24780  xrge0tsms  24791  cnmptre  24889  icchmeo  24906  icchmeoOLD  24907  bndth  24925  lebnumlem2  24929  cfilresi  25263  causs  25266  bcthlem5  25296  evthicc  25428  ovolficcss  25438  ovolmge0  25446  ovolgelb  25449  ovollb2lem  25457  ovollb2  25458  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliunlem2  25472  ovoliun  25474  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem4  25489  ovolicc2  25491  voliunlem2  25520  voliunlem3  25521  ioombl1lem2  25528  ioombl1lem4  25530  uniioovol  25548  uniiccvol  25549  uniioombllem1  25550  uniioombllem2  25552  uniioombllem3  25554  uniioombllem4  25555  uniioombllem6  25557  dyadmbllem  25568  dyadmbl  25569  volcn  25575  vitalilem4  25580  vitalilem5  25581  cnmbf  25628  i1fmul  25665  itg1addlem4  25668  itg2seq  25711  dvbssntr  25869  dvreslem  25878  dvcjbr  25921  dvferm1  25957  dvferm2  25959  cmvth  25963  cmvthOLD  25964  dvlip  25966  lhop1lem  25986  lhop2  25988  lhop  25989  dvcnvrelem2  25991  dvcnvre  25992  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1a  26012  ftc1lem3  26013  ftc1lem6  26016  itgsubstlem  26023  itgpowd  26025  mdegleb  26037  mdeglt  26038  mdegldg  26039  mdegxrcl  26040  mdegcl  26042  deg1mul3le  26090  ig1pdvds  26153  plyeq0lem  26183  aannenlem2  26305  aalioulem3  26310  taylf  26336  taylthlem2  26350  taylthlem2OLD  26351  pserulm  26399  psercn2  26400  psercn2OLD  26401  psercn  26404  reeff1olem  26424  efcvx  26427  loglesqrt  26739  rlimcnp  26943  xrlimcnp  26946  jensen  26967  wilthlem2  27047  vmadivsumb  27462  pntrsumo1  27544  pntlem3  27588  noseqrdgfn  28314  bdaypw2n0bndlem  28471  perpln2  28795  axcontlem10  29058  usgrexmplef  29344  dfpth2  29814  nmoxr  30854  nmooge0  30855  nmoolb  30859  nmoubi  30860  ubthlem1  30958  shmodi  31478  nmopxr  31954  nmfnxr  31967  nmoplb  31995  nmopub  31996  nmfnlb  32012  nmfnleub  32013  nmopun  32102  branmfn  32193  mdslj1i  32407  hatomistici  32450  xppreima2  32741  fsuppcurry1  32814  fsuppcurry2  32815  fpwrelmap  32823  infxrge0gelb  32857  gsumpart  33157  xrge0tsmsd  33167  pmtrcnel2  33184  cyc3genpm  33246  elrgspnsubrunlem1  33341  elrgspnsubrunlem2  33342  1fldgenq  33416  ssdifidllem  33549  ssmxidllem  33566  mplmulmvr  33716  zarcmplem  34059  metideq  34071  metider  34072  pstmfval  34074  esumgect  34268  esum2d  34271  sigaclci  34310  insiga  34315  omssubadd  34478  eulerpartlemgs2  34558  ballotlemsima  34694  signsply0  34729  iblidicc  34770  fsum2dsub  34785  reprsuc  34793  reprgt  34799  bnj1145  35169  bnj1137  35171  bnj1136  35173  resconn  35462  cvmliftlem8  35508  cvmlift3lem6  35540  mclsssvlem  35778  mclsind  35786  mclsppslem  35799  ivthALT  36551  neibastop1  36575  topjoin  36581  bj-imdirco  37445  ptrecube  37871  poimirlem6  37877  poimirlem15  37886  heicant  37906  mblfinlem2  37909  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  itg2gt0cn  37926  ftc1cnnc  37943  ftc1anclem3  37946  ftc1anclem7  37950  ftc1anclem8  37951  ftc1anc  37952  areacirclem2  37960  areacirclem3  37961  areacirclem4  37962  totbndbnd  38040  prdsbnd  38044  heiborlem1  38062  rrnequiv  38086  reheibor  38090  iccbnd  38091  pmapssbaN  40136  2polssN  40291  paddunN  40303  poldmj1N  40304  ispsubcl2N  40323  psubclinN  40324  paddatclN  40325  poml4N  40329  diaglbN  41431  diaintclN  41434  dibglbN  41542  dibintclN  41543  dicssdvh  41562  dihvalrel  41655  dochexmidlem4  41839  infdesc  43001  ttac  43393  hbtlem6  43486  hbt  43487  cnvssb  43942  cnvrcl0  43981  cnvtrrel  44026  relexpaddss  44074  cotrcltrcl  44081  cotrclrcl  44098  frege96d  44105  frege97d  44108  frege109d  44113  frege131d  44120  rfovcnvf1od  44360  isotone2  44405  gneispace  44490  k0004ss1  44507  grumnudlem  44641  uzfissfz  45685  suplesup  45698  ssrexr  45790  limciccioolb  45981  limcicciooub  45995  limcleqr  46002  cnrefiisplem  46187  cncfiooicclem1  46251  ibliccsinexp  46309  iblioosinexp  46311  itgcoscmulx  46327  itgsincmulx  46332  itgsubsticclem  46333  itgiccshift  46338  itgperiod  46339  itgsbtaddcnst  46340  stoweidlem34  46392  stoweidlem59  46417  dirkeritg  46460  dirkercncflem2  46462  fourierdlem20  46485  fourierdlem31  46496  fourierdlem39  46504  fourierdlem42  46507  fourierdlem46  46510  fourierdlem52  46516  fourierdlem53  46517  fourierdlem60  46524  fourierdlem61  46525  fourierdlem62  46526  fourierdlem68  46532  fourierdlem76  46540  fourierdlem85  46549  fourierdlem88  46552  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem93  46557  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fouriersw  46589  etransclem46  46638  etransclem48  46640  sge0less  46750  sge0resplit  46764  sge0isum  46785  pimdecfgtioo  47075  pimincfltioo  47076  iccpartipre  47781  bgoldbtbndlem2  48166  setrec1lem4  50049  setrec2fun  50051