Theorem sstrdi 3950

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3923

This theorem is used by:  difss2  4092  ssinss1  4198  rintn0  5077  eqbrrdva  5857  ssxpb  6174  relcnvtrg  6270  resssxp  6274  relfld  6279  funssxp  6738  dff2  7098  dff3  7099  fliftf  7319  1stcof  8018  2ndcof  8019  frxp2  8142  frxp3  8149  frrlem13  8297  nnunifi  9254  elfiun  9393  marypha1lem  9396  marypha1  9397  ordtypelem7  9489  tcmin  9711  unwf  9785  rankfu  9852  tcrank  9859  aceq3lem  10116  dfac12lem2  10140  ackbij1lem9  10222  ackbij1lem10  10223  ackbij1lem16  10229  fin23lem26  10320  fin23lem27  10323  fin1a2lem6  10400  itunitc  10416  axdc3lem2  10446  ttukeylem5  10508  fpwwe2lem12  10638  canthwelem  10646  pwfseqlem4  10658  wunex2  10734  wunex3  10737  inar1  10771  inatsk  10774  gruina  10814  suprfinzcl  12722  suprzub  12975  uzsupss  12976  uzwo3  12979  rpnnen1lem4  13016  rpnnen1lem5  13017  supxrre  13365  infxrre  13375  ioodisj  13521  supicclub2  13543  fzssnn  13609  fzossnn0  13732  elfzom1elp1fzo  13774  injresinjlem  13832  uzindi  14032  ssnn0fi  14035  seqcoll  14515  seqcoll2  14516  reltrclfv  15074  relexpdmg  15099  relexpdm  15100  relexprng  15103  relexprn  15104  relexpfld  15106  relexpaddg  15110  limsupval2  15551  limsupgre  15552  limsupbnd2  15554  rlimuni  15621  rlimcld2  15649  rlimno1  15725  isercolllem2  15737  isercoll  15739  summolem2a  15785  summolem2  15786  fsumsers  15798  fsumcvg3  15799  prodmolem2a  16007  prodmolem2  16008  zprod  16010  lcmfnnval  16700  lcmfnncl  16705  prmdvdsbc  16803  4sqlem11  17033  vdwlem8  17066  vdwlem11  17069  ramub2  17092  0ram  17098  0ram2  17099  0ramcl  17101  ramub1lem2  17105  prmgaplem3  17131  prmgaplem4  17132  isohom  17851  funcres2c  17978  resscntz  19427  cntzidss  19434  cntzmhm2  19436  pgpssslw  19708  cntzspan  19938  gsumval3  20001  gsum2d  20066  dprdspan  20123  dprdres  20124  subdrgint  20936  sdrgint  20937  primefld  20938  lssintcl  21115  lbsextlem2  21313  lbsextlem3  21314  lbsextlem4  21315  ssdifidllem  21514  islinds3  22014  fctop  23191  cctop  23193  neitr  23367  ordtbas2  23378  ordtopn1  23381  ordtopn2  23382  lmss  23485  clsconn  23617  2ndcdisj  23644  2ndcomap  23646  ptbasfi  23769  txcmplem2  23830  hausdiag  23833  txkgen  23840  basqtop  23899  alexsubb  24234  alexsubALTlem4  24238  tsmsres  24332  tsmsxplem1  24341  tsmsxp  24343  ustrel  24400  utop3cls  24439  prdsmet  24558  metustrel  24740  icccmplem2  25012  xrge0tsms  25023  cnmptre  25117  icchmeo  25131  bndth  25148  lebnumlem2  25152  cfilresi  25485  causs  25488  bcthlem5  25518  evthicc  25649  ovolficcss  25659  ovolmge0  25667  ovolgelb  25670  ovollb2lem  25678  ovollb2  25679  ovolunlem1a  25686  ovolunlem1  25687  ovoliunlem1  25692  ovoliunlem2  25693  ovoliun  25695  ovolscalem1  25703  ovolicc1  25706  ovolicc2lem4  25710  ovolicc2  25712  voliunlem2  25741  voliunlem3  25742  ioombl1lem2  25749  ioombl1lem4  25751  uniioovol  25769  uniiccvol  25770  uniioombllem1  25771  uniioombllem2  25773  uniioombllem3  25775  uniioombllem4  25776  uniioombllem6  25778  dyadmbllem  25789  dyadmbl  25790  volcn  25796  vitalilem4  25801  vitalilem5  25802  cnmbf  25849  i1fmul  25886  itg1addlem4  25889  itg2seq  25932  dvbssntr  26090  dvreslem  26099  dvcjbr  26139  dvferm1  26175  dvferm2  26177  cmvth  26181  dvlip  26183  lhop1lem  26203  lhop2  26205  lhop  26206  dvcnvrelem2  26208  dvcnvre  26209  dvfsumle  26211  dvfsumge  26212  dvfsumabs  26213  dvfsumlem2  26217  ftc1a  26227  ftc1lem3  26228  ftc1lem6  26231  itgsubstlem  26238  itgpowd  26240  mdegleb  26252  mdeglt  26253  mdegldg  26254  mdegxrcl  26255  mdegcl  26257  deg1mul3le  26305  ig1pdvds  26368  plyeq0lem  26398  aannenlem2  26523  aalioulem3  26528  taylf  26555  taylthlem2  26568  pserulm  26616  psercn2  26617  psercn  26620  reeff1olem  26640  efcvx  26643  loglesqrt  26957  rlimcnp  27161  xrlimcnp  27164  jensen  27184  wilthlem2  27264  vmadivsumb  27678  pntrsumo1  27760  pntlem3  27804  noseqrdgfn  28530  bdaypw2n0bndlem  28687  perpln2  29022  axcontlem10  29354  usgrexmplef  29643  dfpth2  30117  nmoxr  31165  nmooge0  31166  nmoolb  31170  nmoubi  31171  ubthlem1  31269  shmodi  31789  nmopxr  32265  nmfnxr  32278  nmoplb  32306  nmopub  32307  nmfnlb  32323  nmfnleub  32324  nmopun  32413  branmfn  32504  mdslj1i  32718  hatomistici  32761  xppreima2  33043  fsuppcurry1  33115  fsuppcurry2  33116  fpwrelmap  33124  infxrge0gelb  33157  gsumpart  33423  xrge0tsmsd  33433  pmtrcnel2  33450  cyc3genpm  33512  elrgspnsubrunlem1  33607  elrgspnsubrunlem2  33608  1fldgenq  33683  ssmxidllem  33796  mplmulmvr  33969  zarcmplem  34311  metideq  34323  metider  34324  pstmfval  34326  esumgect  34520  esum2d  34523  sigaclci  34562  insiga  34568  omssubadd  34731  eulerpartlemgs2  34811  ballotlemsima  34947  signsply0  34979  iblidicc  35020  fsum2dsub  35035  reprsuc  35043  reprgt  35049  bnj1145  35422  bnj1137  35424  bnj1136  35426  resconn  35751  cvmliftlem8  35797  cvmlift3lem6  35829  mclsssvlem  36067  mclsind  36075  mclsppslem  36088  ivthALT  36879  neibastop1  36903  topjoin  36909  dfttc2g  37050  bj-imdirco  37867  ptrecube  38304  poimirlem6  38310  poimirlem15  38319  heicant  38339  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  ismblfin  38345  itg2gt0cn  38359  ftc1cnnc  38376  ftc1anclem3  38379  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  areacirclem2  38393  areacirclem3  38394  areacirclem4  38395  totbndbnd  38473  prdsbnd  38477  heiborlem1  38495  rrnequiv  38519  reheibor  38523  iccbnd  38524  pmapssbaN  40567  2polssN  40722  paddunN  40734  poldmj1N  40735  ispsubcl2N  40754  psubclinN  40755  paddatclN  40756  poml4N  40760  diaglbN  41862  diaintclN  41865  dibglbN  41973  dibintclN  41974  dicssdvh  41993  dihvalrel  42086  dochexmidlem4  42270  infdesc  43408  ttac  43796  hbtlem6  43889  hbt  43890  cnvssb  44345  cnvrcl0  44384  cnvtrrel  44429  relexpaddss  44477  cotrcltrcl  44484  cotrclrcl  44501  frege96d  44508  frege97d  44511  frege109d  44516  frege131d  44523  rfovcnvf1od  44763  isotone2  44808  gneispace  44893  k0004ss1  44910  grumnudlem  45028  uzfissfz  46075  suplesup  46088  ssrexr  46179  limciccioolb  46370  limcicciooub  46384  limcleqr  46391  cnrefiisplem  46576  cncfiooicclem1  46640  ibliccsinexp  46698  iblioosinexp  46700  itgcoscmulx  46716  itgsincmulx  46721  itgsubsticclem  46722  itgiccshift  46727  itgperiod  46728  itgsbtaddcnst  46729  stoweidlem34  46781  stoweidlem59  46806  dirkeritg  46849  dirkercncflem2  46851  fourierdlem20  46874  fourierdlem31  46885  fourierdlem39  46893  fourierdlem42  46896  fourierdlem46  46899  fourierdlem52  46905  fourierdlem53  46906  fourierdlem60  46913  fourierdlem61  46914  fourierdlem62  46915  fourierdlem68  46921  fourierdlem76  46929  fourierdlem85  46938  fourierdlem88  46941  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem93  46946  fourierdlem94  46947  fourierdlem103  46956  fourierdlem104  46957  fourierdlem111  46964  fouriersw  46978  etransclem46  47027  etransclem48  47029  sge0less  47139  sge0resplit  47153  sge0isum  47174  hoicvr  47295  pimdecfgtioo  47464  pimincfltioo  47465  iccpartipre  48203  bgoldbtbndlem2  48604  setrec1lem4  50501  setrec2fun  50503