Theorem sstrdi 3961

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

Syntax hints:   → wi 4   ⊆ wss 3916

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 3933

This theorem is referenced by:  difss2  4103  rintn0  5075  eqbrrdva  5835  ssxpb  6149  resssxp  6245  relfld  6250  funssxp  6718  dff2  7073  dff3  7074  fliftf  7292  1stcof  8000  2ndcof  8001  frxp2  8125  frxp3  8132  frrlem13  8279  nnunifi  9244  elfiun  9387  marypha1lem  9390  marypha1  9391  ordtypelem7  9483  tcmin  9700  unwf  9769  rankfu  9836  tcrank  9843  aceq3lem  10079  dfac12lem2  10104  ackbij1lem9  10186  ackbij1lem10  10187  ackbij1lem16  10193  fin23lem26  10284  fin23lem27  10287  fin1a2lem6  10364  itunitc  10380  axdc3lem2  10410  ttukeylem5  10472  fpwwe2lem12  10601  canthwelem  10609  pwfseqlem4  10621  wunex2  10697  wunex3  10700  inar1  10734  inatsk  10737  gruina  10777  suprfinzcl  12654  suprzub  12904  uzsupss  12905  uzwo3  12908  rpnnen1lem4  12945  rpnnen1lem5  12946  supxrre  13293  infxrre  13303  ioodisj  13449  supicclub2  13471  fzssnn  13535  fzossnn0  13657  elfzom1elp1fzo  13699  injresinjlem  13754  uzindi  13953  ssnn0fi  13956  seqcoll  14435  seqcoll2  14436  reltrclfv  14989  relexpdmg  15014  relexpdm  15015  relexprng  15018  relexprn  15019  relexpfld  15021  relexpaddg  15025  limsupval2  15452  limsupgre  15453  limsupbnd2  15455  rlimuni  15522  rlimcld2  15550  rlimno1  15626  isercolllem2  15638  isercoll  15640  summolem2a  15687  summolem2  15688  fsumsers  15700  fsumcvg3  15701  prodmolem2a  15906  prodmolem2  15907  zprod  15909  lcmfnnval  16600  lcmfnncl  16605  prmdvdsbc  16702  4sqlem11  16932  vdwlem8  16965  vdwlem11  16968  ramub2  16991  0ram  16997  0ram2  16998  0ramcl  17000  ramub1lem2  17004  prmgaplem3  17030  prmgaplem4  17031  isohom  17744  funcres2c  17871  resscntz  19271  cntzidss  19278  cntzmhm2  19280  pgpssslw  19550  cntzspan  19780  gsumval3  19843  gsum2d  19908  dprdspan  19965  dprdres  19966  subdrgint  20718  sdrgint  20719  primefld  20720  lssintcl  20876  lbsextlem2  21075  lbsextlem3  21076  lbsextlem4  21077  islinds3  21749  fctop  22897  cctop  22899  neitr  23073  ordtbas2  23084  ordtopn1  23087  ordtopn2  23088  lmss  23191  clsconn  23323  2ndcdisj  23349  2ndcomap  23351  ptbasfi  23474  txcmplem2  23535  hausdiag  23538  txkgen  23545  basqtop  23604  alexsubb  23939  alexsubALTlem4  23943  tsmsres  24037  tsmsxplem1  24046  tsmsxp  24048  ustrel  24105  utop3cls  24145  prdsmet  24264  metustrel  24446  icccmplem2  24718  xrge0tsms  24729  cnmptre  24827  icchmeo  24844  icchmeoOLD  24845  bndth  24863  lebnumlem2  24867  cfilresi  25201  causs  25204  bcthlem5  25234  evthicc  25366  ovolficcss  25376  ovolmge0  25384  ovolgelb  25387  ovollb2lem  25395  ovollb2  25396  ovolunlem1a  25403  ovolunlem1  25404  ovoliunlem1  25409  ovoliunlem2  25410  ovoliun  25412  ovolscalem1  25420  ovolicc1  25423  ovolicc2lem4  25427  ovolicc2  25429  voliunlem2  25458  voliunlem3  25459  ioombl1lem2  25466  ioombl1lem4  25468  uniioovol  25486  uniiccvol  25487  uniioombllem1  25488  uniioombllem2  25490  uniioombllem3  25492  uniioombllem4  25493  uniioombllem6  25495  dyadmbllem  25506  dyadmbl  25507  volcn  25513  vitalilem4  25518  vitalilem5  25519  cnmbf  25566  i1fmul  25603  itg1addlem4  25606  itg2seq  25649  dvbssntr  25807  dvreslem  25816  dvcjbr  25859  dvferm1  25895  dvferm2  25897  cmvth  25901  cmvthOLD  25902  dvlip  25904  lhop1lem  25924  lhop2  25926  lhop  25927  dvcnvrelem2  25929  dvcnvre  25930  dvfsumle  25932  dvfsumleOLD  25933  dvfsumge  25934  dvfsumabs  25935  dvfsumlem2  25939  dvfsumlem2OLD  25940  ftc1a  25950  ftc1lem3  25951  ftc1lem6  25954  itgsubstlem  25961  itgpowd  25963  mdegleb  25975  mdeglt  25976  mdegldg  25977  mdegxrcl  25978  mdegcl  25980  deg1mul3le  26028  ig1pdvds  26091  plyeq0lem  26121  aannenlem2  26243  aalioulem3  26248  taylf  26274  taylthlem2  26288  taylthlem2OLD  26289  pserulm  26337  psercn2  26338  psercn2OLD  26339  psercn  26342  reeff1olem  26362  efcvx  26365  loglesqrt  26677  rlimcnp  26881  xrlimcnp  26884  jensen  26905  wilthlem2  26985  vmadivsumb  27400  pntrsumo1  27482  pntlem3  27526  noseqrdgfn  28206  perpln2  28644  axcontlem10  28906  usgrexmplef  29192  dfpth2  29665  nmoxr  30701  nmooge0  30702  nmoolb  30706  nmoubi  30707  ubthlem1  30805  shmodi  31325  nmopxr  31801  nmfnxr  31814  nmoplb  31842  nmopub  31843  nmfnlb  31859  nmfnleub  31860  nmopun  31949  branmfn  32040  mdslj1i  32254  hatomistici  32297  xppreima2  32581  fsuppcurry1  32654  fsuppcurry2  32655  fpwrelmap  32662  infxrge0gelb  32695  gsumpart  33003  xrge0tsmsd  33008  pmtrcnel2  33053  cyc3genpm  33115  elrgspnsubrunlem1  33204  elrgspnsubrunlem2  33205  1fldgenq  33278  ssdifidllem  33433  ssmxidllem  33450  zarcmplem  33877  metideq  33889  metider  33890  pstmfval  33892  esumgect  34086  esum2d  34089  sigaclci  34128  insiga  34133  omssubadd  34297  eulerpartlemgs2  34377  ballotlemsima  34513  signsply0  34548  iblidicc  34589  fsum2dsub  34604  reprsuc  34612  reprgt  34618  bnj1145  34989  bnj1137  34991  bnj1136  34993  resconn  35233  cvmliftlem8  35279  cvmlift3lem6  35311  mclsssvlem  35549  mclsind  35557  mclsppslem  35570  ivthALT  36318  neibastop1  36342  topjoin  36348  bj-imdirco  37173  ptrecube  37609  poimirlem6  37615  poimirlem15  37624  heicant  37644  mblfinlem2  37647  mblfinlem3  37648  mblfinlem4  37649  ismblfin  37650  itg2gt0cn  37664  ftc1cnnc  37681  ftc1anclem3  37684  ftc1anclem7  37688  ftc1anclem8  37689  ftc1anc  37690  areacirclem2  37698  areacirclem3  37699  areacirclem4  37700  totbndbnd  37778  prdsbnd  37782  heiborlem1  37800  rrnequiv  37824  reheibor  37828  iccbnd  37829  pmapssbaN  39749  2polssN  39904  paddunN  39916  poldmj1N  39917  ispsubcl2N  39936  psubclinN  39937  paddatclN  39938  poml4N  39942  diaglbN  41044  diaintclN  41047  dibglbN  41155  dibintclN  41156  dicssdvh  41175  dihvalrel  41268  dochexmidlem4  41452  infdesc  42624  rmxyelqirrOLD  42892  ttac  43018  hbtlem6  43111  hbt  43112  cnvssb  43568  cnvrcl0  43607  cnvtrrel  43652  relexpaddss  43700  cotrcltrcl  43707  cotrclrcl  43724  frege96d  43731  frege97d  43734  frege109d  43739  frege131d  43746  rfovcnvf1od  43986  isotone2  44031  gneispace  44116  k0004ss1  44133  grumnudlem  44267  uzfissfz  45315  suplesup  45328  ssrexr  45421  limciccioolb  45612  limcicciooub  45628  limcleqr  45635  cnrefiisplem  45820  cncfiooicclem1  45884  ibliccsinexp  45942  iblioosinexp  45944  itgcoscmulx  45960  itgsincmulx  45965  itgsubsticclem  45966  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  stoweidlem34  46025  stoweidlem59  46050  dirkeritg  46093  dirkercncflem2  46095  fourierdlem20  46118  fourierdlem31  46129  fourierdlem39  46137  fourierdlem42  46140  fourierdlem46  46143  fourierdlem52  46149  fourierdlem53  46150  fourierdlem60  46157  fourierdlem61  46158  fourierdlem62  46159  fourierdlem68  46165  fourierdlem76  46173  fourierdlem85  46182  fourierdlem88  46185  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem93  46190  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fouriersw  46222  etransclem46  46271  etransclem48  46273  sge0less  46383  sge0resplit  46397  sge0isum  46418  pimdecfgtioo  46708  pimincfltioo  46709  iccpartipre  47412  bgoldbtbndlem2  47797  setrec1lem4  49669  setrec2fun  49671