Theorem sstrdi 3929

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

Syntax hints:   → wi 4   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  difss2  4064  rintn0  5034  eqbrrdva  5767  ssxpb  6066  resssxp  6162  relfld  6167  funssxp  6613  dff2  6957  dff3  6958  fliftf  7166  1stcof  7834  2ndcof  7835  frrlem13  8085  nnunifi  8995  elfiun  9119  marypha1lem  9122  marypha1  9123  ordtypelem7  9213  tcmin  9430  unwf  9499  rankfu  9566  tcrank  9573  aceq3lem  9807  dfac12lem2  9831  ackbij1lem9  9915  ackbij1lem10  9916  ackbij1lem16  9922  fin23lem26  10012  fin23lem27  10015  fin1a2lem6  10092  itunitc  10108  axdc3lem2  10138  ttukeylem5  10200  fpwwe2lem12  10329  canthwelem  10337  pwfseqlem4  10349  wunex2  10425  wunex3  10428  inar1  10462  inatsk  10465  gruina  10505  suprfinzcl  12365  suprzub  12608  uzsupss  12609  uzwo3  12612  rpnnen1lem4  12649  rpnnen1lem5  12650  supxrre  12990  infxrre  12999  ioodisj  13143  supicclub2  13165  fzssnn  13229  fzossnn0  13346  elfzom1elp1fzo  13382  injresinjlem  13435  uzindi  13630  ssnn0fi  13633  seqcoll  14106  seqcoll2  14107  reltrclfv  14656  relexpdmg  14681  relexpdm  14682  relexprng  14685  relexprn  14686  relexpfld  14688  relexpaddg  14692  limsupval2  15117  limsupgre  15118  limsupbnd2  15120  rlimuni  15187  rlimcld2  15215  rlimno1  15293  isercolllem2  15305  isercoll  15307  summolem2a  15355  summolem2  15356  fsumsers  15368  fsumcvg3  15369  prodmolem2a  15572  prodmolem2  15573  zprod  15575  lcmfnnval  16257  lcmfnncl  16262  4sqlem11  16584  vdwlem8  16617  vdwlem11  16620  ramub2  16643  0ram  16649  0ram2  16650  0ramcl  16652  ramub1lem2  16656  prmgaplem3  16682  prmgaplem4  16683  isohom  17405  funcres2c  17533  resscntz  18853  cntzidss  18859  cntzmhm2  18861  pgpssslw  19134  cntzspan  19360  gsumval3  19423  gsum2d  19488  dprdspan  19545  dprdres  19546  subdrgint  19986  sdrgint  19987  primefld  19988  lssintcl  20141  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  islinds3  20951  fctop  22062  cctop  22064  neitr  22239  ordtbas2  22250  ordtopn1  22253  ordtopn2  22254  lmss  22357  clsconn  22489  2ndcdisj  22515  2ndcomap  22517  ptbasfi  22640  txcmplem2  22701  hausdiag  22704  txkgen  22711  basqtop  22770  alexsubb  23105  alexsubALTlem4  23109  tsmsres  23203  tsmsxplem1  23212  tsmsxp  23214  ustrel  23271  utop3cls  23311  prdsmet  23431  metustrel  23614  icccmplem2  23892  xrge0tsms  23903  cnmptre  23996  icchmeo  24010  bndth  24027  lebnumlem2  24031  cfilresi  24364  causs  24367  bcthlem5  24397  evthicc  24528  ovolficcss  24538  ovolmge0  24546  ovolgelb  24549  ovollb2lem  24557  ovollb2  24558  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliunlem2  24572  ovoliun  24574  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem4  24589  ovolicc2  24591  voliunlem2  24620  voliunlem3  24621  ioombl1lem2  24628  ioombl1lem4  24630  uniioovol  24648  uniiccvol  24649  uniioombllem1  24650  uniioombllem2  24652  uniioombllem3  24654  uniioombllem4  24655  uniioombllem6  24657  dyadmbllem  24668  dyadmbl  24669  volcn  24675  vitalilem4  24680  vitalilem5  24681  cnmbf  24728  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  itg2seq  24812  dvbssntr  24969  dvreslem  24978  dvcjbr  25018  dvferm1  25054  dvferm2  25056  cmvth  25060  dvlip  25062  lhop1lem  25082  lhop2  25084  lhop  25085  dvcnvrelem2  25087  dvcnvre  25088  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvfsumlem2  25096  ftc1a  25106  ftc1lem3  25107  ftc1lem6  25110  itgsubstlem  25117  itgpowd  25119  mdegleb  25134  mdeglt  25135  mdegldg  25136  mdegxrcl  25137  mdegcl  25139  deg1mul3le  25186  ig1pdvds  25246  plyeq0lem  25276  aannenlem2  25394  aalioulem3  25399  taylf  25425  taylthlem2  25438  pserulm  25486  psercn2  25487  psercn  25490  reeff1olem  25510  efcvx  25513  loglesqrt  25816  rlimcnp  26020  xrlimcnp  26023  jensen  26043  wilthlem2  26123  vmadivsumb  26536  pntrsumo1  26618  pntlem3  26662  perpln2  26976  axcontlem10  27244  usgrexmplef  27529  nmoxr  29029  nmooge0  29030  nmoolb  29034  nmoubi  29035  ubthlem1  29133  shmodi  29653  nmopxr  30129  nmfnxr  30142  nmoplb  30170  nmopub  30171  nmfnlb  30187  nmfnleub  30188  nmopun  30277  branmfn  30368  mdslj1i  30582  hatomistici  30625  xppreima2  30889  fsuppcurry1  30962  fsuppcurry2  30963  fpwrelmap  30970  infxrge0gelb  30991  prmdvdsbc  31032  gsumpart  31217  xrge0tsmsd  31219  pmtrcnel2  31261  cyc3genpm  31321  ssmxidllem  31543  zarcmplem  31733  metideq  31745  metider  31746  pstmfval  31748  esumgect  31958  esum2d  31961  sigaclci  32000  insiga  32005  omssubadd  32167  eulerpartlemgs2  32247  ballotlemsima  32382  signsply0  32430  iblidicc  32472  fsum2dsub  32487  reprsuc  32495  reprgt  32501  bnj1145  32873  bnj1137  32875  bnj1136  32877  resconn  33108  cvmliftlem8  33154  cvmlift3lem6  33186  mclsssvlem  33424  mclsind  33432  mclsppslem  33445  frxp2  33718  frxp3  33724  ivthALT  34451  neibastop1  34475  topjoin  34481  bj-imdirco  35288  ptrecube  35704  poimirlem6  35710  poimirlem15  35719  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anclem3  35779  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirclem2  35793  areacirclem3  35794  areacirclem4  35795  totbndbnd  35874  prdsbnd  35878  heiborlem1  35896  rrnequiv  35920  reheibor  35924  iccbnd  35925  pmapssbaN  37701  2polssN  37856  paddunN  37868  poldmj1N  37869  ispsubcl2N  37888  psubclinN  37889  paddatclN  37890  poml4N  37894  diaglbN  38996  diaintclN  38999  dibglbN  39107  dibintclN  39108  dicssdvh  39127  dihvalrel  39220  dochexmidlem4  39404  infdesc  40396  rmxyelqirr  40648  ttac  40774  hbtlem6  40870  hbt  40871  cnvssb  41083  cnvrcl0  41122  cnvtrrel  41167  relexpaddss  41215  cotrcltrcl  41222  cotrclrcl  41239  frege96d  41246  frege97d  41249  frege109d  41254  frege131d  41261  rfovcnvf1od  41501  isotone2  41548  gneispace  41633  k0004ss1  41650  grumnudlem  41792  uzfissfz  42755  suplesup  42768  ssrexr  42862  limciccioolb  43052  limcicciooub  43068  limcleqr  43075  cnrefiisplem  43260  cncfiooicclem1  43324  ibliccsinexp  43382  iblioosinexp  43384  itgcoscmulx  43400  itgsincmulx  43405  itgsubsticclem  43406  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem34  43465  stoweidlem59  43490  dirkeritg  43533  dirkercncflem2  43535  fourierdlem20  43558  fourierdlem31  43569  fourierdlem39  43577  fourierdlem42  43580  fourierdlem46  43583  fourierdlem52  43589  fourierdlem53  43590  fourierdlem60  43597  fourierdlem61  43598  fourierdlem62  43599  fourierdlem68  43605  fourierdlem76  43613  fourierdlem85  43622  fourierdlem88  43625  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem93  43630  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fouriersw  43662  etransclem46  43711  etransclem48  43713  sge0less  43820  sge0resplit  43834  sge0isum  43855  pimdecfgtioo  44141  pimincfltioo  44142  iccpartipre  44761  bgoldbtbndlem2  45146  setrec1lem4  46282  setrec2fun  46284