Theorem sstrdi 3942

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

Syntax hints:   → wi 4   ⊆ wss 3897

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3914

This theorem is referenced by:  difss2  4083  rintn0  5052  eqbrrdva  5804  ssxpb  6116  resssxp  6212  relfld  6217  funssxp  6674  dff2  7027  dff3  7028  fliftf  7244  1stcof  7946  2ndcof  7947  frxp2  8069  frxp3  8076  frrlem13  8223  nnunifi  9170  elfiun  9309  marypha1lem  9312  marypha1  9313  ordtypelem7  9405  tcmin  9624  unwf  9698  rankfu  9765  tcrank  9772  aceq3lem  10006  dfac12lem2  10031  ackbij1lem9  10113  ackbij1lem10  10114  ackbij1lem16  10120  fin23lem26  10211  fin23lem27  10214  fin1a2lem6  10291  itunitc  10307  axdc3lem2  10337  ttukeylem5  10399  fpwwe2lem12  10528  canthwelem  10536  pwfseqlem4  10548  wunex2  10624  wunex3  10627  inar1  10661  inatsk  10664  gruina  10704  suprfinzcl  12582  suprzub  12832  uzsupss  12833  uzwo3  12836  rpnnen1lem4  12873  rpnnen1lem5  12874  supxrre  13221  infxrre  13231  ioodisj  13377  supicclub2  13399  fzssnn  13463  fzossnn0  13585  elfzom1elp1fzo  13627  injresinjlem  13685  uzindi  13884  ssnn0fi  13887  seqcoll  14366  seqcoll2  14367  reltrclfv  14919  relexpdmg  14944  relexpdm  14945  relexprng  14948  relexprn  14949  relexpfld  14951  relexpaddg  14955  limsupval2  15382  limsupgre  15383  limsupbnd2  15385  rlimuni  15452  rlimcld2  15480  rlimno1  15556  isercolllem2  15568  isercoll  15570  summolem2a  15617  summolem2  15618  fsumsers  15630  fsumcvg3  15631  prodmolem2a  15836  prodmolem2  15837  zprod  15839  lcmfnnval  16530  lcmfnncl  16535  prmdvdsbc  16632  4sqlem11  16862  vdwlem8  16895  vdwlem11  16898  ramub2  16921  0ram  16927  0ram2  16928  0ramcl  16930  ramub1lem2  16934  prmgaplem3  16960  prmgaplem4  16961  isohom  17678  funcres2c  17805  resscntz  19240  cntzidss  19247  cntzmhm2  19249  pgpssslw  19521  cntzspan  19751  gsumval3  19814  gsum2d  19879  dprdspan  19936  dprdres  19937  subdrgint  20713  sdrgint  20714  primefld  20715  lssintcl  20892  lbsextlem2  21091  lbsextlem3  21092  lbsextlem4  21093  islinds3  21766  fctop  22914  cctop  22916  neitr  23090  ordtbas2  23101  ordtopn1  23104  ordtopn2  23105  lmss  23208  clsconn  23340  2ndcdisj  23366  2ndcomap  23368  ptbasfi  23491  txcmplem2  23552  hausdiag  23555  txkgen  23562  basqtop  23621  alexsubb  23956  alexsubALTlem4  23960  tsmsres  24054  tsmsxplem1  24063  tsmsxp  24065  ustrel  24122  utop3cls  24161  prdsmet  24280  metustrel  24462  icccmplem2  24734  xrge0tsms  24745  cnmptre  24843  icchmeo  24860  icchmeoOLD  24861  bndth  24879  lebnumlem2  24883  cfilresi  25217  causs  25220  bcthlem5  25250  evthicc  25382  ovolficcss  25392  ovolmge0  25400  ovolgelb  25403  ovollb2lem  25411  ovollb2  25412  ovolunlem1a  25419  ovolunlem1  25420  ovoliunlem1  25425  ovoliunlem2  25426  ovoliun  25428  ovolscalem1  25436  ovolicc1  25439  ovolicc2lem4  25443  ovolicc2  25445  voliunlem2  25474  voliunlem3  25475  ioombl1lem2  25482  ioombl1lem4  25484  uniioovol  25502  uniiccvol  25503  uniioombllem1  25504  uniioombllem2  25506  uniioombllem3  25508  uniioombllem4  25509  uniioombllem6  25511  dyadmbllem  25522  dyadmbl  25523  volcn  25529  vitalilem4  25534  vitalilem5  25535  cnmbf  25582  i1fmul  25619  itg1addlem4  25622  itg2seq  25665  dvbssntr  25823  dvreslem  25832  dvcjbr  25875  dvferm1  25911  dvferm2  25913  cmvth  25917  cmvthOLD  25918  dvlip  25920  lhop1lem  25940  lhop2  25942  lhop  25943  dvcnvrelem2  25945  dvcnvre  25946  dvfsumle  25948  dvfsumleOLD  25949  dvfsumge  25950  dvfsumabs  25951  dvfsumlem2  25955  dvfsumlem2OLD  25956  ftc1a  25966  ftc1lem3  25967  ftc1lem6  25970  itgsubstlem  25977  itgpowd  25979  mdegleb  25991  mdeglt  25992  mdegldg  25993  mdegxrcl  25994  mdegcl  25996  deg1mul3le  26044  ig1pdvds  26107  plyeq0lem  26137  aannenlem2  26259  aalioulem3  26264  taylf  26290  taylthlem2  26304  taylthlem2OLD  26305  pserulm  26353  psercn2  26354  psercn2OLD  26355  psercn  26358  reeff1olem  26378  efcvx  26381  loglesqrt  26693  rlimcnp  26897  xrlimcnp  26900  jensen  26921  wilthlem2  27001  vmadivsumb  27416  pntrsumo1  27498  pntlem3  27542  noseqrdgfn  28231  perpln2  28684  axcontlem10  28946  usgrexmplef  29232  dfpth2  29702  nmoxr  30738  nmooge0  30739  nmoolb  30743  nmoubi  30744  ubthlem1  30842  shmodi  31362  nmopxr  31838  nmfnxr  31851  nmoplb  31879  nmopub  31880  nmfnlb  31896  nmfnleub  31897  nmopun  31986  branmfn  32077  mdslj1i  32291  hatomistici  32334  xppreima2  32625  fsuppcurry1  32699  fsuppcurry2  32700  fpwrelmap  32708  infxrge0gelb  32741  gsumpart  33029  xrge0tsmsd  33034  pmtrcnel2  33051  cyc3genpm  33113  elrgspnsubrunlem1  33206  elrgspnsubrunlem2  33207  1fldgenq  33280  ssdifidllem  33413  ssmxidllem  33430  zarcmplem  33886  metideq  33898  metider  33899  pstmfval  33901  esumgect  34095  esum2d  34098  sigaclci  34137  insiga  34142  omssubadd  34305  eulerpartlemgs2  34385  ballotlemsima  34521  signsply0  34556  iblidicc  34597  fsum2dsub  34612  reprsuc  34620  reprgt  34626  bnj1145  34997  bnj1137  34999  bnj1136  35001  resconn  35282  cvmliftlem8  35328  cvmlift3lem6  35360  mclsssvlem  35598  mclsind  35606  mclsppslem  35619  ivthALT  36369  neibastop1  36393  topjoin  36399  bj-imdirco  37224  ptrecube  37660  poimirlem6  37666  poimirlem15  37675  heicant  37695  mblfinlem2  37698  mblfinlem3  37699  mblfinlem4  37700  ismblfin  37701  itg2gt0cn  37715  ftc1cnnc  37732  ftc1anclem3  37735  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  areacirclem2  37749  areacirclem3  37750  areacirclem4  37751  totbndbnd  37829  prdsbnd  37833  heiborlem1  37851  rrnequiv  37875  reheibor  37879  iccbnd  37880  pmapssbaN  39799  2polssN  39954  paddunN  39966  poldmj1N  39967  ispsubcl2N  39986  psubclinN  39987  paddatclN  39988  poml4N  39992  diaglbN  41094  diaintclN  41097  dibglbN  41205  dibintclN  41206  dicssdvh  41225  dihvalrel  41318  dochexmidlem4  41502  infdesc  42676  ttac  43069  hbtlem6  43162  hbt  43163  cnvssb  43619  cnvrcl0  43658  cnvtrrel  43703  relexpaddss  43751  cotrcltrcl  43758  cotrclrcl  43775  frege96d  43782  frege97d  43785  frege109d  43790  frege131d  43797  rfovcnvf1od  44037  isotone2  44082  gneispace  44167  k0004ss1  44184  grumnudlem  44318  uzfissfz  45365  suplesup  45378  ssrexr  45470  limciccioolb  45661  limcicciooub  45675  limcleqr  45682  cnrefiisplem  45867  cncfiooicclem1  45931  ibliccsinexp  45989  iblioosinexp  45991  itgcoscmulx  46007  itgsincmulx  46012  itgsubsticclem  46013  itgiccshift  46018  itgperiod  46019  itgsbtaddcnst  46020  stoweidlem34  46072  stoweidlem59  46097  dirkeritg  46140  dirkercncflem2  46142  fourierdlem20  46165  fourierdlem31  46176  fourierdlem39  46184  fourierdlem42  46187  fourierdlem46  46190  fourierdlem52  46196  fourierdlem53  46197  fourierdlem60  46204  fourierdlem61  46205  fourierdlem62  46206  fourierdlem68  46212  fourierdlem76  46220  fourierdlem85  46229  fourierdlem88  46232  fourierdlem89  46233  fourierdlem90  46234  fourierdlem91  46235  fourierdlem93  46237  fourierdlem94  46238  fourierdlem103  46247  fourierdlem104  46248  fourierdlem111  46255  fouriersw  46269  etransclem46  46318  etransclem48  46320  sge0less  46430  sge0resplit  46444  sge0isum  46465  pimdecfgtioo  46755  pimincfltioo  46756  iccpartipre  47452  bgoldbtbndlem2  47837  setrec1lem4  49722  setrec2fun  49724