Theorem sstrdi 4007

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

Syntax hints:   → wi 4   ⊆ wss 3962

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

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

This theorem is referenced by:  difss2  4147  rintn0  5113  eqbrrdva  5882  ssxpb  6195  resssxp  6291  relfld  6296  funssxp  6764  dff2  7118  dff3  7119  fliftf  7334  1stcof  8042  2ndcof  8043  frxp2  8167  frxp3  8174  frrlem13  8321  nnunifi  9324  elfiun  9467  marypha1lem  9470  marypha1  9471  ordtypelem7  9561  tcmin  9778  unwf  9847  rankfu  9914  tcrank  9921  aceq3lem  10157  dfac12lem2  10182  ackbij1lem9  10264  ackbij1lem10  10265  ackbij1lem16  10271  fin23lem26  10362  fin23lem27  10365  fin1a2lem6  10442  itunitc  10458  axdc3lem2  10488  ttukeylem5  10550  fpwwe2lem12  10679  canthwelem  10687  pwfseqlem4  10699  wunex2  10775  wunex3  10778  inar1  10812  inatsk  10815  gruina  10855  suprfinzcl  12729  suprzub  12978  uzsupss  12979  uzwo3  12982  rpnnen1lem4  13019  rpnnen1lem5  13020  supxrre  13365  infxrre  13374  ioodisj  13518  supicclub2  13540  fzssnn  13604  fzossnn0  13726  elfzom1elp1fzo  13767  injresinjlem  13822  uzindi  14019  ssnn0fi  14022  seqcoll  14499  seqcoll2  14500  reltrclfv  15052  relexpdmg  15077  relexpdm  15078  relexprng  15081  relexprn  15082  relexpfld  15084  relexpaddg  15088  limsupval2  15512  limsupgre  15513  limsupbnd2  15515  rlimuni  15582  rlimcld2  15610  rlimno1  15686  isercolllem2  15698  isercoll  15700  summolem2a  15747  summolem2  15748  fsumsers  15760  fsumcvg3  15761  prodmolem2a  15966  prodmolem2  15967  zprod  15969  lcmfnnval  16657  lcmfnncl  16662  prmdvdsbc  16759  4sqlem11  16988  vdwlem8  17021  vdwlem11  17024  ramub2  17047  0ram  17053  0ram2  17054  0ramcl  17056  ramub1lem2  17060  prmgaplem3  17086  prmgaplem4  17087  isohom  17823  funcres2c  17954  resscntz  19363  cntzidss  19370  cntzmhm2  19372  pgpssslw  19646  cntzspan  19876  gsumval3  19939  gsum2d  20004  dprdspan  20061  dprdres  20062  subdrgint  20820  sdrgint  20821  primefld  20822  lssintcl  20979  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  islinds3  21871  fctop  23026  cctop  23028  neitr  23203  ordtbas2  23214  ordtopn1  23217  ordtopn2  23218  lmss  23321  clsconn  23453  2ndcdisj  23479  2ndcomap  23481  ptbasfi  23604  txcmplem2  23665  hausdiag  23668  txkgen  23675  basqtop  23734  alexsubb  24069  alexsubALTlem4  24073  tsmsres  24167  tsmsxplem1  24176  tsmsxp  24178  ustrel  24235  utop3cls  24275  prdsmet  24395  metustrel  24580  icccmplem2  24858  xrge0tsms  24869  cnmptre  24967  icchmeo  24984  icchmeoOLD  24985  bndth  25003  lebnumlem2  25007  cfilresi  25342  causs  25345  bcthlem5  25375  evthicc  25507  ovolficcss  25517  ovolmge0  25525  ovolgelb  25528  ovollb2lem  25536  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliunlem2  25551  ovoliun  25553  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem4  25568  ovolicc2  25570  voliunlem2  25599  voliunlem3  25600  ioombl1lem2  25607  ioombl1lem4  25609  uniioovol  25627  uniiccvol  25628  uniioombllem1  25629  uniioombllem2  25631  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  dyadmbllem  25647  dyadmbl  25648  volcn  25654  vitalilem4  25659  vitalilem5  25660  cnmbf  25707  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  itg2seq  25791  dvbssntr  25949  dvreslem  25958  dvcjbr  26001  dvferm1  26037  dvferm2  26039  cmvth  26043  cmvthOLD  26044  dvlip  26046  lhop1lem  26066  lhop2  26068  lhop  26069  dvcnvrelem2  26071  dvcnvre  26072  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  ftc1a  26092  ftc1lem3  26093  ftc1lem6  26096  itgsubstlem  26103  itgpowd  26105  mdegleb  26117  mdeglt  26118  mdegldg  26119  mdegxrcl  26120  mdegcl  26122  deg1mul3le  26170  ig1pdvds  26233  plyeq0lem  26263  aannenlem2  26385  aalioulem3  26390  taylf  26416  taylthlem2  26430  taylthlem2OLD  26431  pserulm  26479  psercn2  26480  psercn2OLD  26481  psercn  26484  reeff1olem  26504  efcvx  26507  loglesqrt  26818  rlimcnp  27022  xrlimcnp  27025  jensen  27046  wilthlem2  27126  vmadivsumb  27541  pntrsumo1  27623  pntlem3  27667  noseqrdgfn  28326  perpln2  28733  axcontlem10  29002  usgrexmplef  29290  nmoxr  30794  nmooge0  30795  nmoolb  30799  nmoubi  30800  ubthlem1  30898  shmodi  31418  nmopxr  31894  nmfnxr  31907  nmoplb  31935  nmopub  31936  nmfnlb  31952  nmfnleub  31953  nmopun  32042  branmfn  32133  mdslj1i  32347  hatomistici  32390  xppreima2  32667  fsuppcurry1  32742  fsuppcurry2  32743  fpwrelmap  32750  infxrge0gelb  32776  gsumpart  33042  xrge0tsmsd  33047  pmtrcnel2  33092  cyc3genpm  33154  1fldgenq  33303  ssdifidllem  33463  ssmxidllem  33480  zarcmplem  33841  metideq  33853  metider  33854  pstmfval  33856  esumgect  34070  esum2d  34073  sigaclci  34112  insiga  34117  omssubadd  34281  eulerpartlemgs2  34361  ballotlemsima  34496  signsply0  34544  iblidicc  34585  fsum2dsub  34600  reprsuc  34608  reprgt  34614  bnj1145  34985  bnj1137  34987  bnj1136  34989  resconn  35230  cvmliftlem8  35276  cvmlift3lem6  35308  mclsssvlem  35546  mclsind  35554  mclsppslem  35567  ivthALT  36317  neibastop1  36341  topjoin  36347  bj-imdirco  37172  ptrecube  37606  poimirlem6  37612  poimirlem15  37621  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anclem3  37681  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirclem2  37695  areacirclem3  37696  areacirclem4  37697  totbndbnd  37775  prdsbnd  37779  heiborlem1  37797  rrnequiv  37821  reheibor  37825  iccbnd  37826  pmapssbaN  39742  2polssN  39897  paddunN  39909  poldmj1N  39910  ispsubcl2N  39929  psubclinN  39930  paddatclN  39931  poml4N  39935  diaglbN  41037  diaintclN  41040  dibglbN  41148  dibintclN  41149  dicssdvh  41168  dihvalrel  41261  dochexmidlem4  41445  infdesc  42629  rmxyelqirrOLD  42898  ttac  43024  hbtlem6  43117  hbt  43118  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  44280  uzfissfz  45275  suplesup  45288  ssrexr  45381  limciccioolb  45576  limcicciooub  45592  limcleqr  45599  cnrefiisplem  45784  cncfiooicclem1  45848  ibliccsinexp  45906  iblioosinexp  45908  itgcoscmulx  45924  itgsincmulx  45929  itgsubsticclem  45930  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem34  45989  stoweidlem59  46014  dirkeritg  46057  dirkercncflem2  46059  fourierdlem20  46082  fourierdlem31  46093  fourierdlem39  46101  fourierdlem42  46104  fourierdlem46  46107  fourierdlem52  46113  fourierdlem53  46114  fourierdlem60  46121  fourierdlem61  46122  fourierdlem62  46123  fourierdlem68  46129  fourierdlem76  46137  fourierdlem85  46146  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem93  46154  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fouriersw  46186  etransclem46  46235  etransclem48  46237  sge0less  46347  sge0resplit  46361  sge0isum  46382  pimdecfgtioo  46672  pimincfltioo  46673  iccpartipre  47345  bgoldbtbndlem2  47730  setrec1lem4  48920  setrec2fun  48922