Theorem sstrdi 3943

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

Syntax hints:   → wi 4   ⊆ wss 3898

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 3915

This theorem is referenced by:  difss2  4087  rintn0  5061  eqbrrdva  5815  ssxpb  6129  resssxp  6225  relfld  6230  funssxp  6687  dff2  7041  dff3  7042  fliftf  7258  1stcof  7960  2ndcof  7961  frxp2  8083  frxp3  8090  frrlem13  8237  nnunifi  9186  elfiun  9325  marypha1lem  9328  marypha1  9329  ordtypelem7  9421  tcmin  9640  unwf  9714  rankfu  9781  tcrank  9788  aceq3lem  10022  dfac12lem2  10047  ackbij1lem9  10129  ackbij1lem10  10130  ackbij1lem16  10136  fin23lem26  10227  fin23lem27  10230  fin1a2lem6  10307  itunitc  10323  axdc3lem2  10353  ttukeylem5  10415  fpwwe2lem12  10544  canthwelem  10552  pwfseqlem4  10564  wunex2  10640  wunex3  10643  inar1  10677  inatsk  10680  gruina  10720  suprfinzcl  12597  suprzub  12843  uzsupss  12844  uzwo3  12847  rpnnen1lem4  12884  rpnnen1lem5  12885  supxrre  13233  infxrre  13243  ioodisj  13389  supicclub2  13411  fzssnn  13475  fzossnn0  13597  elfzom1elp1fzo  13639  injresinjlem  13697  uzindi  13896  ssnn0fi  13899  seqcoll  14378  seqcoll2  14379  reltrclfv  14931  relexpdmg  14956  relexpdm  14957  relexprng  14960  relexprn  14961  relexpfld  14963  relexpaddg  14967  limsupval2  15394  limsupgre  15395  limsupbnd2  15397  rlimuni  15464  rlimcld2  15492  rlimno1  15568  isercolllem2  15580  isercoll  15582  summolem2a  15629  summolem2  15630  fsumsers  15642  fsumcvg3  15643  prodmolem2a  15848  prodmolem2  15849  zprod  15851  lcmfnnval  16542  lcmfnncl  16547  prmdvdsbc  16644  4sqlem11  16874  vdwlem8  16907  vdwlem11  16910  ramub2  16933  0ram  16939  0ram2  16940  0ramcl  16942  ramub1lem2  16946  prmgaplem3  16972  prmgaplem4  16973  isohom  17691  funcres2c  17818  resscntz  19253  cntzidss  19260  cntzmhm2  19262  pgpssslw  19534  cntzspan  19764  gsumval3  19827  gsum2d  19892  dprdspan  19949  dprdres  19950  subdrgint  20727  sdrgint  20728  primefld  20729  lssintcl  20906  lbsextlem2  21105  lbsextlem3  21106  lbsextlem4  21107  islinds3  21780  fctop  22939  cctop  22941  neitr  23115  ordtbas2  23126  ordtopn1  23129  ordtopn2  23130  lmss  23233  clsconn  23365  2ndcdisj  23391  2ndcomap  23393  ptbasfi  23516  txcmplem2  23577  hausdiag  23580  txkgen  23587  basqtop  23646  alexsubb  23981  alexsubALTlem4  23985  tsmsres  24079  tsmsxplem1  24088  tsmsxp  24090  ustrel  24147  utop3cls  24186  prdsmet  24305  metustrel  24487  icccmplem2  24759  xrge0tsms  24770  cnmptre  24868  icchmeo  24885  icchmeoOLD  24886  bndth  24904  lebnumlem2  24908  cfilresi  25242  causs  25245  bcthlem5  25275  evthicc  25407  ovolficcss  25417  ovolmge0  25425  ovolgelb  25428  ovollb2lem  25436  ovollb2  25437  ovolunlem1a  25444  ovolunlem1  25445  ovoliunlem1  25450  ovoliunlem2  25451  ovoliun  25453  ovolscalem1  25461  ovolicc1  25464  ovolicc2lem4  25468  ovolicc2  25470  voliunlem2  25499  voliunlem3  25500  ioombl1lem2  25507  ioombl1lem4  25509  uniioovol  25527  uniiccvol  25528  uniioombllem1  25529  uniioombllem2  25531  uniioombllem3  25533  uniioombllem4  25534  uniioombllem6  25536  dyadmbllem  25547  dyadmbl  25548  volcn  25554  vitalilem4  25559  vitalilem5  25560  cnmbf  25607  i1fmul  25644  itg1addlem4  25647  itg2seq  25690  dvbssntr  25848  dvreslem  25857  dvcjbr  25900  dvferm1  25936  dvferm2  25938  cmvth  25942  cmvthOLD  25943  dvlip  25945  lhop1lem  25965  lhop2  25967  lhop  25968  dvcnvrelem2  25970  dvcnvre  25971  dvfsumle  25973  dvfsumleOLD  25974  dvfsumge  25975  dvfsumabs  25976  dvfsumlem2  25980  dvfsumlem2OLD  25981  ftc1a  25991  ftc1lem3  25992  ftc1lem6  25995  itgsubstlem  26002  itgpowd  26004  mdegleb  26016  mdeglt  26017  mdegldg  26018  mdegxrcl  26019  mdegcl  26021  deg1mul3le  26069  ig1pdvds  26132  plyeq0lem  26162  aannenlem2  26284  aalioulem3  26289  taylf  26315  taylthlem2  26329  taylthlem2OLD  26330  pserulm  26378  psercn2  26379  psercn2OLD  26380  psercn  26383  reeff1olem  26403  efcvx  26406  loglesqrt  26718  rlimcnp  26922  xrlimcnp  26925  jensen  26946  wilthlem2  27026  vmadivsumb  27441  pntrsumo1  27523  pntlem3  27567  noseqrdgfn  28256  perpln2  28709  axcontlem10  28972  usgrexmplef  29258  dfpth2  29728  nmoxr  30767  nmooge0  30768  nmoolb  30772  nmoubi  30773  ubthlem1  30871  shmodi  31391  nmopxr  31867  nmfnxr  31880  nmoplb  31908  nmopub  31909  nmfnlb  31925  nmfnleub  31926  nmopun  32015  branmfn  32106  mdslj1i  32320  hatomistici  32363  xppreima2  32655  fsuppcurry1  32731  fsuppcurry2  32732  fpwrelmap  32740  infxrge0gelb  32774  gsumpart  33074  xrge0tsmsd  33083  pmtrcnel2  33100  cyc3genpm  33162  elrgspnsubrunlem1  33257  elrgspnsubrunlem2  33258  1fldgenq  33332  ssdifidllem  33465  ssmxidllem  33482  mplmulmvr  33632  zarcmplem  33966  metideq  33978  metider  33979  pstmfval  33981  esumgect  34175  esum2d  34178  sigaclci  34217  insiga  34222  omssubadd  34385  eulerpartlemgs2  34465  ballotlemsima  34601  signsply0  34636  iblidicc  34677  fsum2dsub  34692  reprsuc  34700  reprgt  34706  bnj1145  35077  bnj1137  35079  bnj1136  35081  resconn  35362  cvmliftlem8  35408  cvmlift3lem6  35440  mclsssvlem  35678  mclsind  35686  mclsppslem  35699  ivthALT  36451  neibastop1  36475  topjoin  36481  bj-imdirco  37307  ptrecube  37733  poimirlem6  37739  poimirlem15  37748  heicant  37768  mblfinlem2  37771  mblfinlem3  37772  mblfinlem4  37773  ismblfin  37774  itg2gt0cn  37788  ftc1cnnc  37805  ftc1anclem3  37808  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  areacirclem2  37822  areacirclem3  37823  areacirclem4  37824  totbndbnd  37902  prdsbnd  37906  heiborlem1  37924  rrnequiv  37948  reheibor  37952  iccbnd  37953  pmapssbaN  39932  2polssN  40087  paddunN  40099  poldmj1N  40100  ispsubcl2N  40119  psubclinN  40120  paddatclN  40121  poml4N  40125  diaglbN  41227  diaintclN  41230  dibglbN  41338  dibintclN  41339  dicssdvh  41358  dihvalrel  41451  dochexmidlem4  41635  infdesc  42801  ttac  43193  hbtlem6  43286  hbt  43287  cnvssb  43743  cnvrcl0  43782  cnvtrrel  43827  relexpaddss  43875  cotrcltrcl  43882  cotrclrcl  43899  frege96d  43906  frege97d  43909  frege109d  43914  frege131d  43921  rfovcnvf1od  44161  isotone2  44206  gneispace  44291  k0004ss1  44308  grumnudlem  44442  uzfissfz  45487  suplesup  45500  ssrexr  45592  limciccioolb  45783  limcicciooub  45797  limcleqr  45804  cnrefiisplem  45989  cncfiooicclem1  46053  ibliccsinexp  46111  iblioosinexp  46113  itgcoscmulx  46129  itgsincmulx  46134  itgsubsticclem  46135  itgiccshift  46140  itgperiod  46141  itgsbtaddcnst  46142  stoweidlem34  46194  stoweidlem59  46219  dirkeritg  46262  dirkercncflem2  46264  fourierdlem20  46287  fourierdlem31  46298  fourierdlem39  46306  fourierdlem42  46309  fourierdlem46  46312  fourierdlem52  46318  fourierdlem53  46319  fourierdlem60  46326  fourierdlem61  46327  fourierdlem62  46328  fourierdlem68  46334  fourierdlem76  46342  fourierdlem85  46351  fourierdlem88  46354  fourierdlem89  46355  fourierdlem90  46356  fourierdlem91  46357  fourierdlem93  46359  fourierdlem94  46360  fourierdlem103  46369  fourierdlem104  46370  fourierdlem111  46377  fouriersw  46391  etransclem46  46440  etransclem48  46442  sge0less  46552  sge0resplit  46566  sge0isum  46587  pimdecfgtioo  46877  pimincfltioo  46878  iccpartipre  47583  bgoldbtbndlem2  47968  setrec1lem4  49851  setrec2fun  49853