Theorem sstrdi 3957

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

Syntax hints:   → wi 4   ⊆ wss 3913

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3930

This theorem is referenced by:  difss2  4100  ssinss1  4206  rintn0  5076  eqbrrdva  5853  ssxpb  6171  resssxp  6268  relfld  6273  funssxp  6732  dff2  7092  dff3  7093  fliftf  7311  1stcof  8012  2ndcof  8013  frxp2  8136  frxp3  8143  frrlem13  8291  nnunifi  9247  elfiun  9386  marypha1lem  9389  marypha1  9390  ordtypelem7  9482  tcmin  9704  unwf  9778  rankfu  9845  tcrank  9852  aceq3lem  10100  dfac12lem2  10124  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1lem16  10213  fin23lem26  10305  fin23lem27  10308  fin1a2lem6  10385  itunitc  10401  axdc3lem2  10431  ttukeylem5  10493  fpwwe2lem12  10623  canthwelem  10631  pwfseqlem4  10643  wunex2  10719  wunex3  10722  inar1  10756  inatsk  10759  gruina  10799  suprfinzcl  12706  suprzub  12959  uzsupss  12960  uzwo3  12963  rpnnen1lem4  13000  rpnnen1lem5  13001  supxrre  13349  infxrre  13359  ioodisj  13505  supicclub2  13527  fzssnn  13592  fzossnn0  13715  elfzom1elp1fzo  13757  injresinjlem  13815  uzindi  14014  ssnn0fi  14017  seqcoll  14497  seqcoll2  14498  reltrclfv  15050  relexpdmg  15075  relexpdm  15076  relexprng  15079  relexprn  15080  relexpfld  15082  relexpaddg  15086  limsupval2  15527  limsupgre  15528  limsupbnd2  15530  rlimuni  15597  rlimcld2  15625  rlimno1  15701  isercolllem2  15713  isercoll  15715  summolem2a  15762  summolem2  15763  fsumsers  15775  fsumcvg3  15776  prodmolem2a  15984  prodmolem2  15985  zprod  15987  lcmfnnval  16678  lcmfnncl  16683  prmdvdsbc  16781  4sqlem11  17011  vdwlem8  17044  vdwlem11  17047  ramub2  17070  0ram  17076  0ram2  17077  0ramcl  17079  ramub1lem2  17083  prmgaplem3  17109  prmgaplem4  17110  isohom  17829  funcres2c  17956  resscntz  19399  cntzidss  19406  cntzmhm2  19408  pgpssslw  19680  cntzspan  19910  gsumval3  19973  gsum2d  20038  dprdspan  20095  dprdres  20096  subdrgint  20880  sdrgint  20881  primefld  20882  lssintcl  21059  lbsextlem2  21257  lbsextlem3  21258  lbsextlem4  21259  ssdifidllem  21449  islinds3  21949  fctop  23126  cctop  23128  neitr  23302  ordtbas2  23313  ordtopn1  23316  ordtopn2  23317  lmss  23420  clsconn  23552  2ndcdisj  23578  2ndcomap  23580  ptbasfi  23703  txcmplem2  23764  hausdiag  23767  txkgen  23774  basqtop  23833  alexsubb  24168  alexsubALTlem4  24172  tsmsres  24266  tsmsxplem1  24275  tsmsxp  24277  ustrel  24334  utop3cls  24373  prdsmet  24492  metustrel  24674  icccmplem2  24946  xrge0tsms  24957  cnmptre  25051  icchmeo  25065  bndth  25082  lebnumlem2  25086  cfilresi  25419  causs  25422  bcthlem5  25452  evthicc  25583  ovolficcss  25593  ovolmge0  25601  ovolgelb  25604  ovollb2lem  25612  ovollb2  25613  ovolunlem1a  25620  ovolunlem1  25621  ovoliunlem1  25626  ovoliunlem2  25627  ovoliun  25629  ovolscalem1  25637  ovolicc1  25640  ovolicc2lem4  25644  ovolicc2  25646  voliunlem2  25675  voliunlem3  25676  ioombl1lem2  25683  ioombl1lem4  25685  uniioovol  25703  uniiccvol  25704  uniioombllem1  25705  uniioombllem2  25707  uniioombllem3  25709  uniioombllem4  25710  uniioombllem6  25712  dyadmbllem  25723  dyadmbl  25724  volcn  25730  vitalilem4  25735  vitalilem5  25736  cnmbf  25783  i1fmul  25820  itg1addlem4  25823  itg2seq  25866  dvbssntr  26024  dvreslem  26033  dvcjbr  26073  dvferm1  26109  dvferm2  26111  cmvth  26115  dvlip  26117  lhop1lem  26137  lhop2  26139  lhop  26140  dvcnvrelem2  26142  dvcnvre  26143  dvfsumle  26145  dvfsumge  26146  dvfsumabs  26147  dvfsumlem2  26151  ftc1a  26161  ftc1lem3  26162  ftc1lem6  26165  itgsubstlem  26172  itgpowd  26174  mdegleb  26186  mdeglt  26187  mdegldg  26188  mdegxrcl  26189  mdegcl  26191  deg1mul3le  26239  ig1pdvds  26302  plyeq0lem  26332  aannenlem2  26455  aalioulem3  26460  taylf  26486  taylthlem2  26499  pserulm  26547  psercn2  26548  psercn  26551  reeff1olem  26571  efcvx  26574  loglesqrt  26888  rlimcnp  27092  xrlimcnp  27095  jensen  27115  wilthlem2  27195  vmadivsumb  27609  pntrsumo1  27691  pntlem3  27735  noseqrdgfn  28461  bdaypw2n0bndlem  28618  perpln2  28946  axcontlem10  29260  usgrexmplef  29546  dfpth2  30015  nmoxr  31055  nmooge0  31056  nmoolb  31060  nmoubi  31061  ubthlem1  31159  shmodi  31679  nmopxr  32155  nmfnxr  32168  nmoplb  32196  nmopub  32197  nmfnlb  32213  nmfnleub  32214  nmopun  32303  branmfn  32394  mdslj1i  32608  hatomistici  32651  xppreima2  32933  fsuppcurry1  33006  fsuppcurry2  33007  fpwrelmap  33015  infxrge0gelb  33048  gsumpart  33320  xrge0tsmsd  33330  pmtrcnel2  33347  cyc3genpm  33409  elrgspnsubrunlem1  33504  elrgspnsubrunlem2  33505  1fldgenq  33582  ssmxidllem  33697  mplmulmvr  33870  zarcmplem  34212  metideq  34224  metider  34225  pstmfval  34227  esumgect  34421  esum2d  34424  sigaclci  34463  insiga  34468  omssubadd  34631  eulerpartlemgs2  34711  ballotlemsima  34847  signsply0  34879  iblidicc  34920  fsum2dsub  34935  reprsuc  34943  reprgt  34949  bnj1145  35322  bnj1137  35324  bnj1136  35326  resconn  35633  cvmliftlem8  35679  cvmlift3lem6  35711  mclsssvlem  35949  mclsind  35957  mclsppslem  35970  ivthALT  36731  neibastop1  36755  topjoin  36761  dfttc2g  36902  bj-imdirco  37717  ptrecube  38154  poimirlem6  38160  poimirlem15  38169  heicant  38189  mblfinlem2  38192  mblfinlem3  38193  mblfinlem4  38194  ismblfin  38195  itg2gt0cn  38209  ftc1cnnc  38226  ftc1anclem3  38229  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  areacirclem2  38243  areacirclem3  38244  areacirclem4  38245  totbndbnd  38323  prdsbnd  38327  heiborlem1  38345  rrnequiv  38369  reheibor  38373  iccbnd  38374  pmapssbaN  40419  2polssN  40574  paddunN  40586  poldmj1N  40587  ispsubcl2N  40606  psubclinN  40607  paddatclN  40608  poml4N  40612  diaglbN  41714  diaintclN  41717  dibglbN  41825  dibintclN  41826  dicssdvh  41845  dihvalrel  41938  dochexmidlem4  42122  infdesc  43260  ttac  43648  hbtlem6  43741  hbt  43742  cnvssb  44197  cnvrcl0  44236  cnvtrrel  44281  relexpaddss  44329  cotrcltrcl  44336  cotrclrcl  44353  frege96d  44360  frege97d  44363  frege109d  44368  frege131d  44375  rfovcnvf1od  44615  isotone2  44660  gneispace  44745  k0004ss1  44762  grumnudlem  44880  uzfissfz  45927  suplesup  45940  ssrexr  46031  limciccioolb  46222  limcicciooub  46236  limcleqr  46243  cnrefiisplem  46428  cncfiooicclem1  46492  ibliccsinexp  46550  iblioosinexp  46552  itgcoscmulx  46568  itgsincmulx  46573  itgsubsticclem  46574  itgiccshift  46579  itgperiod  46580  itgsbtaddcnst  46581  stoweidlem34  46633  stoweidlem59  46658  dirkeritg  46701  dirkercncflem2  46703  fourierdlem20  46726  fourierdlem31  46737  fourierdlem39  46745  fourierdlem42  46748  fourierdlem46  46751  fourierdlem52  46757  fourierdlem53  46758  fourierdlem60  46765  fourierdlem61  46766  fourierdlem62  46767  fourierdlem68  46773  fourierdlem76  46781  fourierdlem85  46790  fourierdlem88  46793  fourierdlem89  46794  fourierdlem90  46795  fourierdlem91  46796  fourierdlem93  46798  fourierdlem94  46799  fourierdlem103  46808  fourierdlem104  46809  fourierdlem111  46816  fouriersw  46830  etransclem46  46879  etransclem48  46881  sge0less  46991  sge0resplit  47005  sge0isum  47026  hoicvr  47147  pimdecfgtioo  47316  pimincfltioo  47317  iccpartipre  48052  bgoldbtbndlem2  48453  setrec1lem4  50346  setrec2fun  50348