Theorem sstrdi 3927

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

Syntax hints:   → wi 4   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3900

This theorem is referenced by:  difss2  4068  rintn0  5038  eqbrrdva  5811  ssxpb  6125  resssxp  6221  relfld  6226  funssxp  6683  dff2  7040  dff3  7041  fliftf  7259  1stcof  7961  2ndcof  7962  frxp2  8084  frxp3  8091  frrlem13  8238  nnunifi  9191  elfiun  9333  marypha1lem  9336  marypha1  9337  ordtypelem7  9429  tcmin  9651  unwf  9725  rankfu  9792  tcrank  9799  aceq3lem  10033  dfac12lem2  10058  ackbij1lem9  10140  ackbij1lem10  10141  ackbij1lem16  10147  fin23lem26  10238  fin23lem27  10241  fin1a2lem6  10318  itunitc  10334  axdc3lem2  10364  ttukeylem5  10426  fpwwe2lem12  10556  canthwelem  10564  pwfseqlem4  10576  wunex2  10652  wunex3  10655  inar1  10689  inatsk  10692  gruina  10732  suprfinzcl  12634  suprzub  12880  uzsupss  12881  uzwo3  12884  rpnnen1lem4  12921  rpnnen1lem5  12922  supxrre  13270  infxrre  13280  ioodisj  13426  supicclub2  13448  fzssnn  13513  fzossnn0  13636  elfzom1elp1fzo  13678  injresinjlem  13736  uzindi  13935  ssnn0fi  13938  seqcoll  14417  seqcoll2  14418  reltrclfv  14970  relexpdmg  14995  relexpdm  14996  relexprng  14999  relexprn  15000  relexpfld  15002  relexpaddg  15006  limsupval2  15433  limsupgre  15434  limsupbnd2  15436  rlimuni  15503  rlimcld2  15531  rlimno1  15607  isercolllem2  15619  isercoll  15621  summolem2a  15668  summolem2  15669  fsumsers  15681  fsumcvg3  15682  prodmolem2a  15890  prodmolem2  15891  zprod  15893  lcmfnnval  16584  lcmfnncl  16589  prmdvdsbc  16687  4sqlem11  16917  vdwlem8  16950  vdwlem11  16953  ramub2  16976  0ram  16982  0ram2  16983  0ramcl  16985  ramub1lem2  16989  prmgaplem3  17015  prmgaplem4  17016  isohom  17734  funcres2c  17861  resscntz  19299  cntzidss  19306  cntzmhm2  19308  pgpssslw  19580  cntzspan  19810  gsumval3  19873  gsum2d  19938  dprdspan  19995  dprdres  19996  subdrgint  20775  sdrgint  20776  primefld  20777  lssintcl  20954  lbsextlem2  21152  lbsextlem3  21153  lbsextlem4  21154  islinds3  21809  fctop  22987  cctop  22989  neitr  23163  ordtbas2  23174  ordtopn1  23177  ordtopn2  23178  lmss  23281  clsconn  23413  2ndcdisj  23439  2ndcomap  23441  ptbasfi  23564  txcmplem2  23625  hausdiag  23628  txkgen  23635  basqtop  23694  alexsubb  24029  alexsubALTlem4  24033  tsmsres  24127  tsmsxplem1  24136  tsmsxp  24138  ustrel  24195  utop3cls  24234  prdsmet  24353  metustrel  24535  icccmplem2  24807  xrge0tsms  24818  cnmptre  24912  icchmeo  24926  bndth  24943  lebnumlem2  24947  cfilresi  25280  causs  25283  bcthlem5  25313  evthicc  25444  ovolficcss  25454  ovolmge0  25462  ovolgelb  25465  ovollb2lem  25473  ovollb2  25474  ovolunlem1a  25481  ovolunlem1  25482  ovoliunlem1  25487  ovoliunlem2  25488  ovoliun  25490  ovolscalem1  25498  ovolicc1  25501  ovolicc2lem4  25505  ovolicc2  25507  voliunlem2  25536  voliunlem3  25537  ioombl1lem2  25544  ioombl1lem4  25546  uniioovol  25564  uniiccvol  25565  uniioombllem1  25566  uniioombllem2  25568  uniioombllem3  25570  uniioombllem4  25571  uniioombllem6  25573  dyadmbllem  25584  dyadmbl  25585  volcn  25591  vitalilem4  25596  vitalilem5  25597  cnmbf  25644  i1fmul  25681  itg1addlem4  25684  itg2seq  25727  dvbssntr  25885  dvreslem  25894  dvcjbr  25934  dvferm1  25970  dvferm2  25972  cmvth  25976  dvlip  25978  lhop1lem  25998  lhop2  26000  lhop  26001  dvcnvrelem2  26003  dvcnvre  26004  dvfsumle  26006  dvfsumge  26007  dvfsumabs  26008  dvfsumlem2  26012  ftc1a  26022  ftc1lem3  26023  ftc1lem6  26026  itgsubstlem  26033  itgpowd  26035  mdegleb  26047  mdeglt  26048  mdegldg  26049  mdegxrcl  26050  mdegcl  26052  deg1mul3le  26100  ig1pdvds  26163  plyeq0lem  26193  aannenlem2  26313  aalioulem3  26318  taylf  26344  taylthlem2  26357  pserulm  26405  psercn2  26406  psercn  26409  reeff1olem  26429  efcvx  26432  loglesqrt  26743  rlimcnp  26947  xrlimcnp  26950  jensen  26970  wilthlem2  27050  vmadivsumb  27464  pntrsumo1  27546  pntlem3  27590  noseqrdgfn  28316  bdaypw2n0bndlem  28473  perpln2  28797  axcontlem10  29060  usgrexmplef  29346  dfpth2  29815  nmoxr  30855  nmooge0  30856  nmoolb  30860  nmoubi  30861  ubthlem1  30959  shmodi  31479  nmopxr  31955  nmfnxr  31968  nmoplb  31996  nmopub  31997  nmfnlb  32013  nmfnleub  32014  nmopun  32103  branmfn  32194  mdslj1i  32408  hatomistici  32451  xppreima2  32743  fsuppcurry1  32816  fsuppcurry2  32817  fpwrelmap  32825  infxrge0gelb  32858  gsumpart  33144  xrge0tsmsd  33154  pmtrcnel2  33171  cyc3genpm  33233  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  1fldgenq  33406  ssdifidllem  33539  ssmxidllem  33556  mplmulmvr  33723  zarcmplem  34065  metideq  34077  metider  34078  pstmfval  34080  esumgect  34274  esum2d  34277  sigaclci  34316  insiga  34321  omssubadd  34484  eulerpartlemgs2  34564  ballotlemsima  34700  signsply0  34735  iblidicc  34776  fsum2dsub  34791  reprsuc  34799  reprgt  34805  bnj1145  35175  bnj1137  35177  bnj1136  35179  resconn  35474  cvmliftlem8  35520  cvmlift3lem6  35552  mclsssvlem  35790  mclsind  35798  mclsppslem  35811  ivthALT  36563  neibastop1  36587  topjoin  36593  dfttc2g  36734  bj-imdirco  37550  ptrecube  37987  poimirlem6  37993  poimirlem15  38002  heicant  38022  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  itg2gt0cn  38042  ftc1cnnc  38059  ftc1anclem3  38062  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  areacirclem2  38076  areacirclem3  38077  areacirclem4  38078  totbndbnd  38156  prdsbnd  38160  heiborlem1  38178  rrnequiv  38202  reheibor  38206  iccbnd  38207  pmapssbaN  40252  2polssN  40407  paddunN  40419  poldmj1N  40420  ispsubcl2N  40439  psubclinN  40440  paddatclN  40441  poml4N  40445  diaglbN  41547  diaintclN  41550  dibglbN  41658  dibintclN  41659  dicssdvh  41678  dihvalrel  41771  dochexmidlem4  41955  infdesc  43093  ttac  43481  hbtlem6  43574  hbt  43575  cnvssb  44030  cnvrcl0  44069  cnvtrrel  44114  relexpaddss  44162  cotrcltrcl  44169  cotrclrcl  44186  frege96d  44193  frege97d  44196  frege109d  44201  frege131d  44208  rfovcnvf1od  44448  isotone2  44493  gneispace  44578  k0004ss1  44595  grumnudlem  44729  uzfissfz  45771  suplesup  45784  ssrexr  45875  limciccioolb  46066  limcicciooub  46080  limcleqr  46087  cnrefiisplem  46272  cncfiooicclem1  46336  ibliccsinexp  46394  iblioosinexp  46396  itgcoscmulx  46412  itgsincmulx  46417  itgsubsticclem  46418  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  stoweidlem34  46477  stoweidlem59  46502  dirkeritg  46545  dirkercncflem2  46547  fourierdlem20  46570  fourierdlem31  46581  fourierdlem39  46589  fourierdlem42  46592  fourierdlem46  46595  fourierdlem52  46601  fourierdlem53  46602  fourierdlem60  46609  fourierdlem61  46610  fourierdlem62  46611  fourierdlem68  46617  fourierdlem76  46625  fourierdlem85  46634  fourierdlem88  46637  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem93  46642  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fouriersw  46674  etransclem46  46723  etransclem48  46725  sge0less  46835  sge0resplit  46849  sge0isum  46870  hoicvr  46991  pimdecfgtioo  47160  pimincfltioo  47161  iccpartipre  47896  bgoldbtbndlem2  48297  setrec1lem4  50180  setrec2fun  50182