Theorem sstrdi 3959

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

Syntax hints:   → wi 4   ⊆ wss 3914

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

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

This theorem is referenced by:  difss2  4101  rintn0  5073  eqbrrdva  5833  ssxpb  6147  resssxp  6243  relfld  6248  funssxp  6716  dff2  7071  dff3  7072  fliftf  7290  1stcof  7998  2ndcof  7999  frxp2  8123  frxp3  8130  frrlem13  8277  nnunifi  9238  elfiun  9381  marypha1lem  9384  marypha1  9385  ordtypelem7  9477  tcmin  9694  unwf  9763  rankfu  9830  tcrank  9837  aceq3lem  10073  dfac12lem2  10098  ackbij1lem9  10180  ackbij1lem10  10181  ackbij1lem16  10187  fin23lem26  10278  fin23lem27  10281  fin1a2lem6  10358  itunitc  10374  axdc3lem2  10404  ttukeylem5  10466  fpwwe2lem12  10595  canthwelem  10603  pwfseqlem4  10615  wunex2  10691  wunex3  10694  inar1  10728  inatsk  10731  gruina  10771  suprfinzcl  12648  suprzub  12898  uzsupss  12899  uzwo3  12902  rpnnen1lem4  12939  rpnnen1lem5  12940  supxrre  13287  infxrre  13297  ioodisj  13443  supicclub2  13465  fzssnn  13529  fzossnn0  13651  elfzom1elp1fzo  13693  injresinjlem  13748  uzindi  13947  ssnn0fi  13950  seqcoll  14429  seqcoll2  14430  reltrclfv  14983  relexpdmg  15008  relexpdm  15009  relexprng  15012  relexprn  15013  relexpfld  15015  relexpaddg  15019  limsupval2  15446  limsupgre  15447  limsupbnd2  15449  rlimuni  15516  rlimcld2  15544  rlimno1  15620  isercolllem2  15632  isercoll  15634  summolem2a  15681  summolem2  15682  fsumsers  15694  fsumcvg3  15695  prodmolem2a  15900  prodmolem2  15901  zprod  15903  lcmfnnval  16594  lcmfnncl  16599  prmdvdsbc  16696  4sqlem11  16926  vdwlem8  16959  vdwlem11  16962  ramub2  16985  0ram  16991  0ram2  16992  0ramcl  16994  ramub1lem2  16998  prmgaplem3  17024  prmgaplem4  17025  isohom  17738  funcres2c  17865  resscntz  19265  cntzidss  19272  cntzmhm2  19274  pgpssslw  19544  cntzspan  19774  gsumval3  19837  gsum2d  19902  dprdspan  19959  dprdres  19960  subdrgint  20712  sdrgint  20713  primefld  20714  lssintcl  20870  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  islinds3  21743  fctop  22891  cctop  22893  neitr  23067  ordtbas2  23078  ordtopn1  23081  ordtopn2  23082  lmss  23185  clsconn  23317  2ndcdisj  23343  2ndcomap  23345  ptbasfi  23468  txcmplem2  23529  hausdiag  23532  txkgen  23539  basqtop  23598  alexsubb  23933  alexsubALTlem4  23937  tsmsres  24031  tsmsxplem1  24040  tsmsxp  24042  ustrel  24099  utop3cls  24139  prdsmet  24258  metustrel  24440  icccmplem2  24712  xrge0tsms  24723  cnmptre  24821  icchmeo  24838  icchmeoOLD  24839  bndth  24857  lebnumlem2  24861  cfilresi  25195  causs  25198  bcthlem5  25228  evthicc  25360  ovolficcss  25370  ovolmge0  25378  ovolgelb  25381  ovollb2lem  25389  ovollb2  25390  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliunlem2  25404  ovoliun  25406  ovolscalem1  25414  ovolicc1  25417  ovolicc2lem4  25421  ovolicc2  25423  voliunlem2  25452  voliunlem3  25453  ioombl1lem2  25460  ioombl1lem4  25462  uniioovol  25480  uniiccvol  25481  uniioombllem1  25482  uniioombllem2  25484  uniioombllem3  25486  uniioombllem4  25487  uniioombllem6  25489  dyadmbllem  25500  dyadmbl  25501  volcn  25507  vitalilem4  25512  vitalilem5  25513  cnmbf  25560  i1fmul  25597  itg1addlem4  25600  itg2seq  25643  dvbssntr  25801  dvreslem  25810  dvcjbr  25853  dvferm1  25889  dvferm2  25891  cmvth  25895  cmvthOLD  25896  dvlip  25898  lhop1lem  25918  lhop2  25920  lhop  25921  dvcnvrelem2  25923  dvcnvre  25924  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1a  25944  ftc1lem3  25945  ftc1lem6  25948  itgsubstlem  25955  itgpowd  25957  mdegleb  25969  mdeglt  25970  mdegldg  25971  mdegxrcl  25972  mdegcl  25974  deg1mul3le  26022  ig1pdvds  26085  plyeq0lem  26115  aannenlem2  26237  aalioulem3  26242  taylf  26268  taylthlem2  26282  taylthlem2OLD  26283  pserulm  26331  psercn2  26332  psercn2OLD  26333  psercn  26336  reeff1olem  26356  efcvx  26359  loglesqrt  26671  rlimcnp  26875  xrlimcnp  26878  jensen  26899  wilthlem2  26979  vmadivsumb  27394  pntrsumo1  27476  pntlem3  27520  noseqrdgfn  28200  perpln2  28638  axcontlem10  28900  usgrexmplef  29186  dfpth2  29659  nmoxr  30695  nmooge0  30696  nmoolb  30700  nmoubi  30701  ubthlem1  30799  shmodi  31319  nmopxr  31795  nmfnxr  31808  nmoplb  31836  nmopub  31837  nmfnlb  31853  nmfnleub  31854  nmopun  31943  branmfn  32034  mdslj1i  32248  hatomistici  32291  xppreima2  32575  fsuppcurry1  32648  fsuppcurry2  32649  fpwrelmap  32656  infxrge0gelb  32689  gsumpart  32997  xrge0tsmsd  33002  pmtrcnel2  33047  cyc3genpm  33109  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  1fldgenq  33272  ssdifidllem  33427  ssmxidllem  33444  zarcmplem  33871  metideq  33883  metider  33884  pstmfval  33886  esumgect  34080  esum2d  34083  sigaclci  34122  insiga  34127  omssubadd  34291  eulerpartlemgs2  34371  ballotlemsima  34507  signsply0  34542  iblidicc  34583  fsum2dsub  34598  reprsuc  34606  reprgt  34612  bnj1145  34983  bnj1137  34985  bnj1136  34987  resconn  35233  cvmliftlem8  35279  cvmlift3lem6  35311  mclsssvlem  35549  mclsind  35557  mclsppslem  35570  ivthALT  36323  neibastop1  36347  topjoin  36353  bj-imdirco  37178  ptrecube  37614  poimirlem6  37620  poimirlem15  37629  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anclem3  37689  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem2  37703  areacirclem3  37704  areacirclem4  37705  totbndbnd  37783  prdsbnd  37787  heiborlem1  37805  rrnequiv  37829  reheibor  37833  iccbnd  37834  pmapssbaN  39754  2polssN  39909  paddunN  39921  poldmj1N  39922  ispsubcl2N  39941  psubclinN  39942  paddatclN  39943  poml4N  39947  diaglbN  41049  diaintclN  41052  dibglbN  41160  dibintclN  41161  dicssdvh  41180  dihvalrel  41273  dochexmidlem4  41457  infdesc  42631  rmxyelqirrOLD  42899  ttac  43025  hbtlem6  43118  hbt  43119  cnvssb  43575  cnvrcl0  43614  cnvtrrel  43659  relexpaddss  43707  cotrcltrcl  43714  cotrclrcl  43731  frege96d  43738  frege97d  43741  frege109d  43746  frege131d  43753  rfovcnvf1od  43993  isotone2  44038  gneispace  44123  k0004ss1  44140  grumnudlem  44274  uzfissfz  45322  suplesup  45335  ssrexr  45428  limciccioolb  45619  limcicciooub  45635  limcleqr  45642  cnrefiisplem  45827  cncfiooicclem1  45891  ibliccsinexp  45949  iblioosinexp  45951  itgcoscmulx  45967  itgsincmulx  45972  itgsubsticclem  45973  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem34  46032  stoweidlem59  46057  dirkeritg  46100  dirkercncflem2  46102  fourierdlem20  46125  fourierdlem31  46136  fourierdlem39  46144  fourierdlem42  46147  fourierdlem46  46150  fourierdlem52  46156  fourierdlem53  46157  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem68  46172  fourierdlem76  46180  fourierdlem85  46189  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem93  46197  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fouriersw  46229  etransclem46  46278  etransclem48  46280  sge0less  46390  sge0resplit  46404  sge0isum  46425  pimdecfgtioo  46715  pimincfltioo  46716  iccpartipre  47422  bgoldbtbndlem2  47807  setrec1lem4  49679  setrec2fun  49681