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

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

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

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

This theorem is used by:  difss2  4085  ssinss1  4191  rintn0  5069  eqbrrdva  5847  ssxpb  6166  relcnvtrg  6267  resssxp  6271  relfld  6276  funssxp  6736  dff2  7097  dff3  7098  fliftf  7321  1stcof  8029  2ndcof  8030  frxp2  8154  frxp3  8161  frrlem13  8309  nnunifi  9276  elfiun  9415  marypha1lem  9418  marypha1  9419  ordtypelem7  9511  tcmin  9733  unwf  9811  rankfu  9887  tcrank  9894  setrec1lem4  9964  setrec2fun  9966  aceq3lem  10192  dfac12lem2  10216  ackbij1lem9  10298  ackbij1lem10  10299  ackbij1lem16  10305  fin23lem26  10396  fin23lem27  10399  fin1a2lem6  10476  itunitc  10492  axdc3lem2  10522  ttukeylem5  10584  fpwwe2lem12  10720  canthwelem  10728  pwfseqlem4  10740  wunex2  10816  wunex3  10819  inar1  10853  inatsk  10856  gruina  10896  suprfinzcl  12806  suprzub  13059  uzsupss  13060  uzwo3  13063  rpnnen1lem4  13101  rpnnen1lem5  13102  supxrre  13450  infxrre  13460  ioodisj  13606  supicclub2  13628  fzssnn  13695  fzossnn0  13818  elfzom1elp1fzo  13860  injresinjlem  13918  uzindi  14118  ssnn0fi  14121  seqcoll  14602  seqcoll2  14603  reltrclfv  15163  relexpdmg  15188  relexpdm  15189  relexprng  15192  relexprn  15193  relexpfld  15195  relexpaddg  15199  limsupval2  15640  limsupgre  15641  limsupbnd2  15643  rlimuni  15710  rlimcld2  15738  rlimno1  15814  isercolllem2  15826  isercoll  15828  summolem2a  15874  summolem2  15875  fsumsers  15887  fsumcvg3  15888  prodmolem2a  16094  prodmolem2  16095  zprod  16097  lcmfnnval  16792  lcmfnncl  16797  prmdvdsbc  16895  4sqlem11  17126  vdwlem8  17159  vdwlem11  17162  ramub2  17185  0ram  17191  0ram2  17192  0ramcl  17194  ramub1lem2  17198  prmgaplem3  17224  prmgaplem4  17225  isohom  17944  funcres2c  18071  resscntz  19540  cntzidss  19547  cntzmhm2  19549  pgpssslw  19821  cntzspan  20051  gsumval3  20114  gsum2d  20179  dprdspan  20236  dprdres  20237  subdrgint  21053  sdrgint  21054  primefld  21055  lssintcl  21232  lbsextlem2  21430  lbsextlem3  21431  lbsextlem4  21432  ssdifidllem  21633  islinds3  22133  fctop  23315  cctop  23317  neitr  23491  ordtbas2  23502  ordtopn1  23505  ordtopn2  23506  lmss  23609  clsconn  23741  2ndcdisj  23768  2ndcomap  23770  ptbasfi  23893  txcmplem2  23954  hausdiag  23957  txkgen  23964  basqtop  24023  alexsubb  24358  alexsubALTlem4  24362  tsmsres  24456  tsmsxplem1  24465  tsmsxp  24467  ustrel  24524  utop3cls  24563  prdsmet  24682  metustrel  24864  icccmplem2  25136  xrge0tsms  25147  cnmptre  25241  icchmeo  25255  bndth  25272  lebnumlem2  25276  cfilresi  25609  causs  25612  bcthlem5  25642  evthicc  25773  ovolficcss  25783  ovolmge0  25791  ovolgelb  25794  ovollb2lem  25802  ovollb2  25803  ovolunlem1a  25810  ovolunlem1  25811  ovoliunlem1  25816  ovoliunlem2  25817  ovoliun  25819  ovolscalem1  25827  ovolicc1  25830  ovolicc2lem4  25834  ovolicc2  25836  voliunlem2  25865  voliunlem3  25866  ioombl1lem2  25873  ioombl1lem4  25875  uniioovol  25893  uniiccvol  25894  uniioombllem1  25895  uniioombllem2  25897  uniioombllem3  25899  uniioombllem4  25900  uniioombllem6  25902  dyadmbllem  25913  dyadmbl  25914  volcn  25920  vitalilem4  25925  vitalilem5  25926  cnmbf  25973  i1fmul  26010  itg1addlem4  26013  itg2seq  26056  dvbssntr  26213  dvreslem  26222  dvcjbr  26262  dvferm1  26298  dvferm2  26300  cmvth  26304  dvlip  26306  lhop1lem  26326  lhop2  26328  lhop  26329  dvcnvrelem2  26331  dvcnvre  26332  dvfsumle  26334  dvfsumge  26335  dvfsumabs  26336  dvfsumlem2  26340  ftc1a  26350  ftc1lem3  26351  ftc1lem6  26354  itgsubstlem  26361  itgpowd  26363  mdegleb  26375  mdeglt  26376  mdegldg  26377  mdegxrcl  26378  mdegcl  26380  deg1mul3le  26428  ig1pdvds  26491  plyeq0lem  26522  aannenlem2  26649  aalioulem3  26654  taylf  26681  taylthlem2  26694  pserulm  26742  psercn2  26743  psercn  26746  reeff1olem  26766  efcvx  26769  loglesqrt  27082  rlimcnp  27286  xrlimcnp  27289  jensen  27309  wilthlem2  27389  vmadivsumb  27803  pntrsumo1  27885  pntlem3  27929  infdesc  27960  noseqrdgfn  28685  bdaypw2n0bndlem  28842  perpln2  29179  axcontlem10  29544  usgrexmplef  29833  dfpth2  30307  nmoxr  31361  nmooge0  31362  nmoolb  31366  nmoubi  31367  ubthlem1  31465  shmodi  31985  nmopxr  32461  nmfnxr  32474  nmoplb  32502  nmopub  32503  nmfnlb  32519  nmfnleub  32520  nmopun  32609  branmfn  32700  mdslj1i  32914  hatomistici  32957  xppreima2  33238  fsuppcurry1  33309  fsuppcurry2  33310  fpwrelmap  33318  infxrge0gelb  33351  gsumpart  33617  xrge0tsmsd  33627  pmtrcnel2  33644  cyc3genpm  33706  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  1fldgenq  33877  ssmxidllem  33991  mplmulmvr  34164  zarcmplem  34506  metideq  34518  metider  34519  pstmfval  34521  esumgect  34715  esum2d  34718  sigaclci  34757  insiga  34763  omssubadd  34925  eulerpartlemgs2  35005  ballotlemsima  35141  signsply0  35173  iblidicc  35214  fsum2dsub  35229  reprsuc  35237  reprgt  35243  bnj1145  35616  bnj1137  35618  bnj1136  35620  resconn  35990  cvmliftlem8  36036  cvmlift3lem6  36068  mclsssvlem  36306  mclsind  36314  mclsppslem  36327  ivthALT  37103  neibastop1  37127  topjoin  37133  dfttc2g  37274  bj-imdirco  38091  ptrecube  38518  poimirlem6  38524  poimirlem15  38533  heicant  38553  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  itg2gt0cn  38573  ftc1cnnc  38590  ftc1anclem3  38593  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  areacirclem2  38607  areacirclem3  38608  areacirclem4  38609  totbndbnd  38703  prdsbnd  38707  heiborlem1  38725  rrnequiv  38749  reheibor  38753  iccbnd  38754  pmapssbaN  40797  2polssN  40952  paddunN  40964  poldmj1N  40965  ispsubcl2N  40984  psubclinN  40985  paddatclN  40986  poml4N  40990  diaglbN  42092  diaintclN  42095  dibglbN  42203  dibintclN  42204  dicssdvh  42223  dihvalrel  42316  dochexmidlem4  42500  frlmnzcoordcl  43635  frlmnzcoordn0  43637  ttac  44022  hbtlem6  44115  hbt  44116  cnvssb  44571  cnvrcl0  44610  cnvtrrel  44655  relexpaddss  44703  cotrcltrcl  44710  cotrclrcl  44727  frege96d  44734  frege97d  44737  frege109d  44742  frege131d  44749  rfovcnvf1od  44989  isotone2  45034  gneispace  45119  k0004ss1  45136  grumnudlem  45254  uzfissfz  46307  suplesup  46320  ssrexr  46411  limciccioolb  46602  limcicciooub  46616  limcleqr  46623  cnrefiisplem  46808  cncfiooicclem1  46872  ibliccsinexp  46930  iblioosinexp  46932  itgcoscmulx  46948  itgsincmulx  46953  itgsubsticclem  46954  itgiccshift  46959  itgperiod  46960  itgsbtaddcnst  46961  stoweidlem34  47013  stoweidlem59  47038  dirkeritg  47081  dirkercncflem2  47083  fourierdlem20  47106  fourierdlem31  47117  fourierdlem39  47125  fourierdlem42  47128  fourierdlem46  47131  fourierdlem52  47137  fourierdlem53  47138  fourierdlem60  47145  fourierdlem61  47146  fourierdlem62  47147  fourierdlem68  47153  fourierdlem76  47161  fourierdlem85  47170  fourierdlem88  47173  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem93  47178  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fouriersw  47210  etransclem46  47259  etransclem48  47261  sge0less  47371  sge0resplit  47385  sge0isum  47406  hoicvr  47527  pimdecfgtioo  47696  pimincfltioo  47697  tmachlem-fssscan  47929  iccpartipre  48472  bgoldbtbndlem2  48873