Theorem sstrdi 3949

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

Syntax hints:   → wi 4   ⊆ wss 3905

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3922

This theorem is referenced by:  difss2  4092  ssinss1  4198  rintn0  5075  eqbrrdva  5855  ssxpb  6172  resssxp  6271  relfld  6276  funssxp  6734  dff2  7094  dff3  7095  fliftf  7313  1stcof  8012  2ndcof  8013  frxp2  8136  frxp3  8143  frrlem13  8291  nnunifi  9247  elfiun  9386  marypha1lem  9389  marypha1  9390  ordtypelem7  9482  tcmin  9704  unwf  9778  rankfu  9845  tcrank  9852  aceq3lem  10100  dfac12lem2  10124  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1lem16  10213  fin23lem26  10304  fin23lem27  10307  fin1a2lem6  10384  itunitc  10400  axdc3lem2  10430  ttukeylem5  10492  fpwwe2lem12  10622  canthwelem  10630  pwfseqlem4  10642  wunex2  10718  wunex3  10721  inar1  10755  inatsk  10758  gruina  10798  suprfinzcl  12705  suprzub  12958  uzsupss  12959  uzwo3  12962  rpnnen1lem4  12999  rpnnen1lem5  13000  supxrre  13348  infxrre  13358  ioodisj  13504  supicclub2  13526  fzssnn  13592  fzossnn0  13715  elfzom1elp1fzo  13757  injresinjlem  13815  uzindi  14014  ssnn0fi  14017  seqcoll  14497  seqcoll2  14498  reltrclfv  15050  relexpdmg  15075  relexpdm  15076  relexprng  15079  relexprn  15080  relexpfld  15082  relexpaddg  15086  limsupval2  15527  limsupgre  15528  limsupbnd2  15530  rlimuni  15597  rlimcld2  15625  rlimno1  15701  isercolllem2  15713  isercoll  15715  summolem2a  15762  summolem2  15763  fsumsers  15775  fsumcvg3  15776  prodmolem2a  15984  prodmolem2  15985  zprod  15987  lcmfnnval  16677  lcmfnncl  16682  prmdvdsbc  16780  4sqlem11  17010  vdwlem8  17043  vdwlem11  17046  ramub2  17069  0ram  17075  0ram2  17076  0ramcl  17078  ramub1lem2  17082  prmgaplem3  17108  prmgaplem4  17109  isohom  17828  funcres2c  17955  resscntz  19398  cntzidss  19405  cntzmhm2  19407  pgpssslw  19679  cntzspan  19909  gsumval3  19972  gsum2d  20037  dprdspan  20094  dprdres  20095  subdrgint  20906  sdrgint  20907  primefld  20908  lssintcl  21085  lbsextlem2  21283  lbsextlem3  21284  lbsextlem4  21285  ssdifidllem  21484  islinds3  21984  fctop  23161  cctop  23163  neitr  23337  ordtbas2  23348  ordtopn1  23351  ordtopn2  23352  lmss  23455  clsconn  23587  2ndcdisj  23613  2ndcomap  23615  ptbasfi  23738  txcmplem2  23799  hausdiag  23802  txkgen  23809  basqtop  23868  alexsubb  24203  alexsubALTlem4  24207  tsmsres  24301  tsmsxplem1  24310  tsmsxp  24312  ustrel  24369  utop3cls  24408  prdsmet  24527  metustrel  24709  icccmplem2  24981  xrge0tsms  24992  cnmptre  25086  icchmeo  25100  bndth  25117  lebnumlem2  25121  cfilresi  25454  causs  25457  bcthlem5  25487  evthicc  25618  ovolficcss  25628  ovolmge0  25636  ovolgelb  25639  ovollb2lem  25647  ovollb2  25648  ovolunlem1a  25655  ovolunlem1  25656  ovoliunlem1  25661  ovoliunlem2  25662  ovoliun  25664  ovolscalem1  25672  ovolicc1  25675  ovolicc2lem4  25679  ovolicc2  25681  voliunlem2  25710  voliunlem3  25711  ioombl1lem2  25718  ioombl1lem4  25720  uniioovol  25738  uniiccvol  25739  uniioombllem1  25740  uniioombllem2  25742  uniioombllem3  25744  uniioombllem4  25745  uniioombllem6  25747  dyadmbllem  25758  dyadmbl  25759  volcn  25765  vitalilem4  25770  vitalilem5  25771  cnmbf  25818  i1fmul  25855  itg1addlem4  25858  itg2seq  25901  dvbssntr  26059  dvreslem  26068  dvcjbr  26108  dvferm1  26144  dvferm2  26146  cmvth  26150  dvlip  26152  lhop1lem  26172  lhop2  26174  lhop  26175  dvcnvrelem2  26177  dvcnvre  26178  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  dvfsumlem2  26186  ftc1a  26196  ftc1lem3  26197  ftc1lem6  26200  itgsubstlem  26207  itgpowd  26209  mdegleb  26221  mdeglt  26222  mdegldg  26223  mdegxrcl  26224  mdegcl  26226  deg1mul3le  26274  ig1pdvds  26337  plyeq0lem  26367  aannenlem2  26492  aalioulem3  26497  taylf  26524  taylthlem2  26537  pserulm  26585  psercn2  26586  psercn  26589  reeff1olem  26609  efcvx  26612  loglesqrt  26926  rlimcnp  27130  xrlimcnp  27133  jensen  27153  wilthlem2  27233  vmadivsumb  27647  pntrsumo1  27729  pntlem3  27773  noseqrdgfn  28499  bdaypw2n0bndlem  28656  perpln2  28991  axcontlem10  29323  usgrexmplef  29609  dfpth2  30078  nmoxr  31118  nmooge0  31119  nmoolb  31123  nmoubi  31124  ubthlem1  31222  shmodi  31742  nmopxr  32218  nmfnxr  32231  nmoplb  32259  nmopub  32260  nmfnlb  32276  nmfnleub  32277  nmopun  32366  branmfn  32457  mdslj1i  32671  hatomistici  32714  xppreima2  32996  fsuppcurry1  33069  fsuppcurry2  33070  fpwrelmap  33078  infxrge0gelb  33111  gsumpart  33383  xrge0tsmsd  33393  pmtrcnel2  33410  cyc3genpm  33472  elrgspnsubrunlem1  33567  elrgspnsubrunlem2  33568  1fldgenq  33643  ssmxidllem  33756  mplmulmvr  33929  zarcmplem  34271  metideq  34283  metider  34284  pstmfval  34286  esumgect  34480  esum2d  34483  sigaclci  34522  insiga  34527  omssubadd  34690  eulerpartlemgs2  34770  ballotlemsima  34906  signsply0  34938  iblidicc  34979  fsum2dsub  34994  reprsuc  35002  reprgt  35008  bnj1145  35381  bnj1137  35383  bnj1136  35385  resconn  35738  cvmliftlem8  35784  cvmlift3lem6  35816  mclsssvlem  36054  mclsind  36062  mclsppslem  36075  ivthALT  36846  neibastop1  36870  topjoin  36876  dfttc2g  37017  bj-imdirco  37834  ptrecube  38271  poimirlem6  38277  poimirlem15  38286  heicant  38306  mblfinlem2  38309  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  itg2gt0cn  38326  ftc1cnnc  38343  ftc1anclem3  38346  ftc1anclem7  38350  ftc1anclem8  38351  ftc1anc  38352  areacirclem2  38360  areacirclem3  38361  areacirclem4  38362  totbndbnd  38440  prdsbnd  38444  heiborlem1  38462  rrnequiv  38486  reheibor  38490  iccbnd  38491  pmapssbaN  40534  2polssN  40689  paddunN  40701  poldmj1N  40702  ispsubcl2N  40721  psubclinN  40722  paddatclN  40723  poml4N  40727  diaglbN  41829  diaintclN  41832  dibglbN  41940  dibintclN  41941  dicssdvh  41960  dihvalrel  42053  dochexmidlem4  42237  infdesc  43375  ttac  43763  hbtlem6  43856  hbt  43857  cnvssb  44312  cnvrcl0  44351  cnvtrrel  44396  relexpaddss  44444  cotrcltrcl  44451  cotrclrcl  44468  frege96d  44475  frege97d  44478  frege109d  44483  frege131d  44490  rfovcnvf1od  44730  isotone2  44775  gneispace  44860  k0004ss1  44877  grumnudlem  44995  uzfissfz  46042  suplesup  46055  ssrexr  46146  limciccioolb  46337  limcicciooub  46351  limcleqr  46358  cnrefiisplem  46543  cncfiooicclem1  46607  ibliccsinexp  46665  iblioosinexp  46667  itgcoscmulx  46683  itgsincmulx  46688  itgsubsticclem  46689  itgiccshift  46694  itgperiod  46695  itgsbtaddcnst  46696  stoweidlem34  46748  stoweidlem59  46773  dirkeritg  46816  dirkercncflem2  46818  fourierdlem20  46841  fourierdlem31  46852  fourierdlem39  46860  fourierdlem42  46863  fourierdlem46  46866  fourierdlem52  46872  fourierdlem53  46873  fourierdlem60  46880  fourierdlem61  46881  fourierdlem62  46882  fourierdlem68  46888  fourierdlem76  46896  fourierdlem85  46905  fourierdlem88  46908  fourierdlem89  46909  fourierdlem90  46910  fourierdlem91  46911  fourierdlem93  46913  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  fouriersw  46945  etransclem46  46994  etransclem48  46996  sge0less  47106  sge0resplit  47120  sge0isum  47141  hoicvr  47262  pimdecfgtioo  47431  pimincfltioo  47432  iccpartipre  48170  bgoldbtbndlem2  48571  setrec1lem4  50468  setrec2fun  50470