Theorem sstrdi 3925

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

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

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 3901

This theorem is used by:  difss2  4077  ssinss1  4145  rintn0  5072  eqbrrdva  5857  ssxpb  6182  cnvssb  6205  relcnvtrg  6290  resssxp  6294  relfld  6299  funssxp  6766  dff2  7129  dff3  7130  fliftf  7352  1stcof  8063  2ndcof  8064  frxp2  8196  frxp3  8203  frrlem13  8352  nnunifi  9319  elfiun  9457  marypha1lem  9460  marypha1  9461  ordtypelem7  9553  tcmin  9775  unwf  9853  rankfu  9929  tcrank  9936  setrec1lem4  10006  setrec2fun  10008  aceq3lem  10236  dfac12lem2  10260  ackbij1lem9  10342  ackbij1lem10  10343  ackbij1lem16  10349  fin23lem26  10440  fin23lem27  10443  fin1a2lem6  10520  itunitc  10536  axdc3lem2  10566  ttukeylem5  10628  fpwwe2lem12  10764  canthwelem  10772  pwfseqlem4  10784  wunex2  10860  wunex3  10863  inar1  10897  inatsk  10900  gruina  10940  suprfinzcl  12851  suprzub  13104  uzsupss  13105  uzwo3  13108  rpnnen1lem4  13146  rpnnen1lem5  13147  supxrre  13495  infxrre  13505  ioodisj  13651  supicclub2  13673  fzssnn  13740  fzossnn0  13863  elfzom1elp1fzo  13905  injresinjlem  13963  uzindi  14163  ssnn0fi  14166  seqcoll  14648  seqcoll2  14649  reltrclfv  15211  relexpdmg  15236  relexpdm  15237  relexprng  15240  relexprn  15241  relexpfld  15243  relexpaddg  15247  limsupval2  15688  limsupgre  15689  limsupbnd2  15691  rlimuni  15758  rlimcld2  15786  rlimno1  15862  isercolllem2  15874  isercoll  15876  summolem2a  15922  summolem2  15923  fsumsers  15935  fsumcvg3  15936  prodmolem2a  16142  prodmolem2  16143  zprod  16145  lcmfnnval  16840  lcmfnncl  16845  prmdvdsbc  16943  4sqlem11  17174  vdwlem8  17207  vdwlem11  17210  ramub2  17233  0ram  17239  0ram2  17240  0ramcl  17242  ramub1lem2  17246  prmgaplem3  17272  prmgaplem4  17273  isohom  17992  funcres2c  18119  resscntz  19589  cntzidss  19596  cntzmhm2  19598  pgpssslw  19870  cntzspan  20100  gsumval3  20163  gsum2d  20228  dprdspan  20285  dprdres  20286  subdrgint  21102  sdrgint  21103  primefld  21104  lssintcl  21281  lbsextlem2  21479  lbsextlem3  21480  lbsextlem4  21481  ssdifidllem  21682  islinds3  22184  fctop  23366  cctop  23368  neitr  23542  ordtbas2  23553  ordtopn1  23556  ordtopn2  23557  lmss  23660  clsconn  23792  2ndcdisj  23819  2ndcomap  23821  ptbasfi  23944  txcmplem2  24005  hausdiag  24008  txkgen  24015  basqtop  24074  alexsubb  24409  alexsubALTlem4  24413  tsmsres  24507  tsmsxplem1  24516  tsmsxp  24518  ustrel  24575  utop3cls  24614  prdsmet  24733  metustrel  24915  icccmplem2  25187  xrge0tsms  25198  cnmptre  25292  icchmeo  25306  bndth  25323  lebnumlem2  25327  cfilresi  25660  causs  25663  bcthlem5  25693  evthicc  25824  ovolficcss  25834  ovolmge0  25842  ovolgelb  25845  ovollb2lem  25853  ovollb2  25854  ovolunlem1a  25861  ovolunlem1  25862  ovoliunlem1  25867  ovoliunlem2  25868  ovoliun  25870  ovolscalem1  25878  ovolicc1  25881  ovolicc2lem4  25885  ovolicc2  25887  voliunlem2  25916  voliunlem3  25917  ioombl1lem2  25924  ioombl1lem4  25926  uniioovol  25944  uniiccvol  25945  uniioombllem1  25946  uniioombllem2  25948  uniioombllem3  25950  uniioombllem4  25951  uniioombllem6  25953  dyadmbllem  25964  dyadmbl  25965  volcn  25971  vitalilem4  25976  vitalilem5  25977  cnmbf  26024  i1fmul  26061  itg1addlem4  26064  itg2seq  26107  dvbssntr  26264  dvreslem  26273  dvcjbr  26313  dvferm1  26349  dvferm2  26351  cmvth  26355  dvlip  26357  lhop1lem  26377  lhop2  26379  lhop  26380  dvcnvrelem2  26382  dvcnvre  26383  dvfsumle  26385  dvfsumge  26386  dvfsumabs  26387  dvfsumlem2  26391  ftc1a  26401  ftc1lem3  26402  ftc1lem6  26405  itgsubstlem  26412  itgpowd  26414  mdegleb  26426  mdeglt  26427  mdegldg  26428  mdegxrcl  26429  mdegcl  26431  deg1mul3le  26479  ig1pdvds  26542  plyeq0lem  26573  aannenlem2  26702  aalioulem3  26707  taylf  26734  taylthlem2  26747  pserulm  26795  psercn2  26796  psercn  26799  reeff1olem  26819  efcvx  26822  loglesqrt  27135  rlimcnp  27339  xrlimcnp  27342  jensen  27362  wilthlem2  27442  vmadivsumb  27856  pntrsumo1  27938  pntlem3  27982  infdesc  28013  noseqrdgfn  28738  bdaypw2n0bndlem  28895  perpln2  29232  axcontlem10  29597  usgrexmplef  29886  dfpth2  30360  nmoxr  31414  nmooge0  31415  nmoolb  31419  nmoubi  31420  ubthlem1  31518  shmodi  32038  nmopxr  32514  nmfnxr  32527  nmoplb  32555  nmopub  32556  nmfnlb  32572  nmfnleub  32573  nmopun  32662  branmfn  32753  mdslj1i  32967  hatomistici  33010  xppreima2  33333  fsuppcurry1  33402  fsuppcurry2  33403  fpwrelmap  33411  infxrge0gelb  33444  gsumpart  33713  xrge0tsmsd  33723  pmtrcnel2  33740  cyc3genpm  33802  elrgspnsubrunlem1  33897  elrgspnsubrunlem2  33898  1fldgenq  33981  ssmxidllem  34095  mplmulmvr  34275  zarcmplem  34617  metideq  34629  metider  34630  pstmfval  34632  esumgect  34826  esum2d  34829  sigaclci  34868  insiga  34874  omssubadd  35036  eulerpartlemgs2  35116  ballotlemsima  35252  signsply0  35284  iblidicc  35325  fsum2dsub  35340  reprsuc  35348  reprgt  35354  bnj1145  35727  bnj1137  35729  bnj1136  35731  resconn  36212  cvmliftlem8  36258  cvmlift3lem6  36290  mclsssvlem  36528  mclsind  36536  mclsppslem  36549  ivthALT  37331  neibastop1  37355  topjoin  37361  dfttc2g  37502  resssres  38171  relssresv  38182  relssdmrnb  38187  relssresb  38188  coindir  38210  coindi  38212  cossidres1  38213  cossidres2  38214  cossidcnvss2  38215  nvo3  38223  bj-imdirco  38372  ptrecube  38799  poimirlem6  38805  poimirlem15  38814  heicant  38834  mblfinlem2  38837  mblfinlem3  38838  mblfinlem4  38839  ismblfin  38840  itg2gt0cn  38854  ftc1cnnc  38871  ftc1anclem3  38874  ftc1anclem7  38878  ftc1anclem8  38879  ftc1anc  38880  areacirclem2  38888  areacirclem3  38889  areacirclem4  38890  totbndbnd  38982  prdsbnd  38986  heiborlem1  39004  rrnequiv  39028  reheibor  39032  iccbnd  39033  pmapssbaN  41076  2polssN  41231  paddunN  41243  poldmj1N  41244  ispsubcl2N  41263  psubclinN  41264  paddatclN  41265  poml4N  41269  diaglbN  42371  diaintclN  42374  dibglbN  42482  dibintclN  42483  dicssdvh  42502  dihvalrel  42595  dochexmidlem4  42779  frlmnzcoordcl  43915  frlmnzcoordn0  43917  ttac  44303  hbtlem6  44390  hbt  44391  cnvrcl0  44880  cnvtrrel  44925  relexpaddss  44973  cotrcltrcl  44980  cotrclrcl  44997  frege96d  45004  frege97d  45007  frege109d  45012  frege131d  45019  rfovcnvf1od  45259  isotone2  45304  gneispace  45389  k0004ss1  45406  grumnudlem  45524  rnhfstructsshf  46288  hfstructcan  46292  uzfissfz  46605  suplesup  46618  ssrexr  46709  limciccioolb  46900  limcicciooub  46914  limcleqr  46921  cnrefiisplem  47106  cncfiooicclem1  47170  ibliccsinexp  47228  iblioosinexp  47230  itgcoscmulx  47246  itgsincmulx  47251  itgsubsticclem  47252  itgiccshift  47257  itgperiod  47258  itgsbtaddcnst  47259  stoweidlem34  47311  stoweidlem59  47336  dirkeritg  47379  dirkercncflem2  47381  fourierdlem20  47404  fourierdlem31  47415  fourierdlem39  47423  fourierdlem42  47426  fourierdlem46  47429  fourierdlem52  47435  fourierdlem53  47436  fourierdlem60  47443  fourierdlem61  47444  fourierdlem62  47445  fourierdlem68  47451  fourierdlem76  47459  fourierdlem85  47468  fourierdlem88  47471  fourierdlem89  47472  fourierdlem90  47473  fourierdlem91  47474  fourierdlem93  47476  fourierdlem94  47477  fourierdlem103  47486  fourierdlem104  47487  fourierdlem111  47494  fouriersw  47508  etransclem46  47557  etransclem48  47559  sge0less  47669  sge0resplit  47683  sge0isum  47704  hoicvr  47825  pimdecfgtioo  47994  pimincfltioo  47995  tmachlem-fssscan  48227  iccpartipre  48770  bgoldbtbndlem2  49171