Theorem sstrdi 3920

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3896

This theorem is used by:  difss2  4074  ssinss1  4142  rintn0  5068  eqbrrdva  5846  ssxpb  6165  cnvssb  6188  relcnvtrg  6268  resssxp  6272  relfld  6277  funssxp  6739  dff2  7100  dff3  7101  fliftf  7324  1stcof  8032  2ndcof  8033  frxp2  8164  frxp3  8171  frrlem13  8320  nnunifi  9287  elfiun  9426  marypha1lem  9429  marypha1  9430  ordtypelem7  9522  tcmin  9744  unwf  9822  rankfu  9898  tcrank  9905  setrec1lem4  9975  setrec2fun  9977  aceq3lem  10203  dfac12lem2  10227  ackbij1lem9  10309  ackbij1lem10  10310  ackbij1lem16  10316  fin23lem26  10407  fin23lem27  10410  fin1a2lem6  10487  itunitc  10503  axdc3lem2  10533  ttukeylem5  10595  fpwwe2lem12  10731  canthwelem  10739  pwfseqlem4  10751  wunex2  10827  wunex3  10830  inar1  10864  inatsk  10867  gruina  10907  suprfinzcl  12817  suprzub  13070  uzsupss  13071  uzwo3  13074  rpnnen1lem4  13112  rpnnen1lem5  13113  supxrre  13461  infxrre  13471  ioodisj  13617  supicclub2  13639  fzssnn  13706  fzossnn0  13829  elfzom1elp1fzo  13871  injresinjlem  13929  uzindi  14129  ssnn0fi  14132  seqcoll  14613  seqcoll2  14614  reltrclfv  15176  relexpdmg  15201  relexpdm  15202  relexprng  15205  relexprn  15206  relexpfld  15208  relexpaddg  15212  limsupval2  15653  limsupgre  15654  limsupbnd2  15656  rlimuni  15723  rlimcld2  15751  rlimno1  15827  isercolllem2  15839  isercoll  15841  summolem2a  15887  summolem2  15888  fsumsers  15900  fsumcvg3  15901  prodmolem2a  16107  prodmolem2  16108  zprod  16110  lcmfnnval  16805  lcmfnncl  16810  prmdvdsbc  16908  4sqlem11  17139  vdwlem8  17172  vdwlem11  17175  ramub2  17198  0ram  17204  0ram2  17205  0ramcl  17207  ramub1lem2  17211  prmgaplem3  17237  prmgaplem4  17238  isohom  17957  funcres2c  18084  resscntz  19553  cntzidss  19560  cntzmhm2  19562  pgpssslw  19834  cntzspan  20064  gsumval3  20127  gsum2d  20192  dprdspan  20249  dprdres  20250  subdrgint  21066  sdrgint  21067  primefld  21068  lssintcl  21245  lbsextlem2  21443  lbsextlem3  21444  lbsextlem4  21445  ssdifidllem  21646  islinds3  22146  fctop  23328  cctop  23330  neitr  23504  ordtbas2  23515  ordtopn1  23518  ordtopn2  23519  lmss  23622  clsconn  23754  2ndcdisj  23781  2ndcomap  23783  ptbasfi  23906  txcmplem2  23967  hausdiag  23970  txkgen  23977  basqtop  24036  alexsubb  24371  alexsubALTlem4  24375  tsmsres  24469  tsmsxplem1  24478  tsmsxp  24480  ustrel  24537  utop3cls  24576  prdsmet  24695  metustrel  24877  icccmplem2  25149  xrge0tsms  25160  cnmptre  25254  icchmeo  25268  bndth  25285  lebnumlem2  25289  cfilresi  25622  causs  25625  bcthlem5  25655  evthicc  25786  ovolficcss  25796  ovolmge0  25804  ovolgelb  25807  ovollb2lem  25815  ovollb2  25816  ovolunlem1a  25823  ovolunlem1  25824  ovoliunlem1  25829  ovoliunlem2  25830  ovoliun  25832  ovolscalem1  25840  ovolicc1  25843  ovolicc2lem4  25847  ovolicc2  25849  voliunlem2  25878  voliunlem3  25879  ioombl1lem2  25886  ioombl1lem4  25888  uniioovol  25906  uniiccvol  25907  uniioombllem1  25908  uniioombllem2  25910  uniioombllem3  25912  uniioombllem4  25913  uniioombllem6  25915  dyadmbllem  25926  dyadmbl  25927  volcn  25933  vitalilem4  25938  vitalilem5  25939  cnmbf  25986  i1fmul  26023  itg1addlem4  26026  itg2seq  26069  dvbssntr  26226  dvreslem  26235  dvcjbr  26275  dvferm1  26311  dvferm2  26313  cmvth  26317  dvlip  26319  lhop1lem  26339  lhop2  26341  lhop  26342  dvcnvrelem2  26344  dvcnvre  26345  dvfsumle  26347  dvfsumge  26348  dvfsumabs  26349  dvfsumlem2  26353  ftc1a  26363  ftc1lem3  26364  ftc1lem6  26367  itgsubstlem  26374  itgpowd  26376  mdegleb  26388  mdeglt  26389  mdegldg  26390  mdegxrcl  26391  mdegcl  26393  deg1mul3le  26441  ig1pdvds  26504  plyeq0lem  26535  aannenlem2  26662  aalioulem3  26667  taylf  26694  taylthlem2  26707  pserulm  26755  psercn2  26756  psercn  26759  reeff1olem  26779  efcvx  26782  loglesqrt  27095  rlimcnp  27299  xrlimcnp  27302  jensen  27322  wilthlem2  27402  vmadivsumb  27816  pntrsumo1  27898  pntlem3  27942  infdesc  27973  noseqrdgfn  28698  bdaypw2n0bndlem  28855  perpln2  29192  axcontlem10  29557  usgrexmplef  29846  dfpth2  30320  nmoxr  31374  nmooge0  31375  nmoolb  31379  nmoubi  31380  ubthlem1  31478  shmodi  31998  nmopxr  32474  nmfnxr  32487  nmoplb  32515  nmopub  32516  nmfnlb  32532  nmfnleub  32533  nmopun  32622  branmfn  32713  mdslj1i  32927  hatomistici  32970  xppreima2  33293  fsuppcurry1  33363  fsuppcurry2  33364  fpwrelmap  33372  infxrge0gelb  33405  gsumpart  33671  xrge0tsmsd  33681  pmtrcnel2  33698  cyc3genpm  33760  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  1fldgenq  33931  ssmxidllem  34045  mplmulmvr  34218  zarcmplem  34560  metideq  34572  metider  34573  pstmfval  34575  esumgect  34769  esum2d  34772  sigaclci  34811  insiga  34817  omssubadd  34979  eulerpartlemgs2  35059  ballotlemsima  35195  signsply0  35227  iblidicc  35268  fsum2dsub  35283  reprsuc  35291  reprgt  35297  bnj1145  35670  bnj1137  35672  bnj1136  35674  resconn  36098  cvmliftlem8  36144  cvmlift3lem6  36176  mclsssvlem  36414  mclsind  36422  mclsppslem  36435  ivthALT  37216  neibastop1  37240  topjoin  37246  dfttc2g  37387  bj-imdirco  38205  ptrecube  38632  poimirlem6  38638  poimirlem15  38647  heicant  38667  mblfinlem2  38670  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  itg2gt0cn  38687  ftc1cnnc  38704  ftc1anclem3  38707  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  areacirclem2  38721  areacirclem3  38722  areacirclem4  38723  totbndbnd  38817  prdsbnd  38821  heiborlem1  38839  rrnequiv  38863  reheibor  38867  iccbnd  38868  pmapssbaN  40911  2polssN  41066  paddunN  41078  poldmj1N  41079  ispsubcl2N  41098  psubclinN  41099  paddatclN  41100  poml4N  41104  diaglbN  42206  diaintclN  42209  dibglbN  42317  dibintclN  42318  dicssdvh  42337  dihvalrel  42430  dochexmidlem4  42614  frlmnzcoordcl  43749  frlmnzcoordn0  43751  ttac  44137  hbtlem6  44225  hbt  44226  cnvrcl0  44719  cnvtrrel  44764  relexpaddss  44812  cotrcltrcl  44819  cotrclrcl  44836  frege96d  44843  frege97d  44846  frege109d  44851  frege131d  44858  rfovcnvf1od  45098  isotone2  45143  gneispace  45228  k0004ss1  45245  grumnudlem  45363  rnhfstructsshf  46121  hfstructcan  46125  uzfissfz  46432  suplesup  46445  ssrexr  46536  limciccioolb  46727  limcicciooub  46741  limcleqr  46748  cnrefiisplem  46933  cncfiooicclem1  46997  ibliccsinexp  47055  iblioosinexp  47057  itgcoscmulx  47073  itgsincmulx  47078  itgsubsticclem  47079  itgiccshift  47084  itgperiod  47085  itgsbtaddcnst  47086  stoweidlem34  47138  stoweidlem59  47163  dirkeritg  47206  dirkercncflem2  47208  fourierdlem20  47231  fourierdlem31  47242  fourierdlem39  47250  fourierdlem42  47253  fourierdlem46  47256  fourierdlem52  47262  fourierdlem53  47263  fourierdlem60  47270  fourierdlem61  47271  fourierdlem62  47272  fourierdlem68  47278  fourierdlem76  47286  fourierdlem85  47295  fourierdlem88  47298  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem93  47303  fourierdlem94  47304  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  fouriersw  47335  etransclem46  47384  etransclem48  47386  sge0less  47496  sge0resplit  47510  sge0isum  47531  hoicvr  47652  pimdecfgtioo  47821  pimincfltioo  47822  tmachlem-fssscan  48054  iccpartipre  48597  bgoldbtbndlem2  48998