Theorem sstrdi 3946

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

Syntax hints:   → wi 4   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3919

This theorem is referenced by:  difss2  4089  ssinss1  4195  rintn0  5063  eqbrrdva  5837  ssxpb  6155  resssxp  6252  relfld  6257  funssxp  6715  dff2  7075  dff3  7076  fliftf  7294  1stcof  7995  2ndcof  7996  frxp2  8118  frxp3  8125  frrlem13  8273  nnunifi  9229  elfiun  9370  marypha1lem  9373  marypha1  9374  ordtypelem7  9466  tcmin  9688  unwf  9762  rankfu  9829  tcrank  9836  aceq3lem  10070  dfac12lem2  10095  ackbij1lem9  10177  ackbij1lem10  10178  ackbij1lem16  10184  fin23lem26  10276  fin23lem27  10279  fin1a2lem6  10356  itunitc  10372  axdc3lem2  10402  ttukeylem5  10464  fpwwe2lem12  10594  canthwelem  10602  pwfseqlem4  10614  wunex2  10690  wunex3  10693  inar1  10727  inatsk  10730  gruina  10770  suprfinzcl  12681  suprzub  12934  uzsupss  12935  uzwo3  12938  rpnnen1lem4  12975  rpnnen1lem5  12976  supxrre  13324  infxrre  13334  ioodisj  13480  supicclub2  13502  fzssnn  13567  fzossnn0  13690  elfzom1elp1fzo  13732  injresinjlem  13790  uzindi  13989  ssnn0fi  13992  seqcoll  14471  seqcoll2  14472  reltrclfv  15024  relexpdmg  15049  relexpdm  15050  relexprng  15053  relexprn  15054  relexpfld  15056  relexpaddg  15060  limsupval2  15498  limsupgre  15499  limsupbnd2  15501  rlimuni  15568  rlimcld2  15596  rlimno1  15672  isercolllem2  15684  isercoll  15686  summolem2a  15733  summolem2  15734  fsumsers  15746  fsumcvg3  15747  prodmolem2a  15955  prodmolem2  15956  zprod  15958  lcmfnnval  16649  lcmfnncl  16654  prmdvdsbc  16752  4sqlem11  16982  vdwlem8  17015  vdwlem11  17018  ramub2  17041  0ram  17047  0ram2  17048  0ramcl  17050  ramub1lem2  17054  prmgaplem3  17080  prmgaplem4  17081  isohom  17800  funcres2c  17927  resscntz  19364  cntzidss  19371  cntzmhm2  19373  pgpssslw  19645  cntzspan  19875  gsumval3  19938  gsum2d  20003  dprdspan  20060  dprdres  20061  subdrgint  20840  sdrgint  20841  primefld  20842  lssintcl  21019  lbsextlem2  21217  lbsextlem3  21218  lbsextlem4  21219  islinds3  21874  fctop  23052  cctop  23054  neitr  23228  ordtbas2  23239  ordtopn1  23242  ordtopn2  23243  lmss  23346  clsconn  23478  2ndcdisj  23504  2ndcomap  23506  ptbasfi  23629  txcmplem2  23690  hausdiag  23693  txkgen  23700  basqtop  23759  alexsubb  24094  alexsubALTlem4  24098  tsmsres  24192  tsmsxplem1  24201  tsmsxp  24203  ustrel  24260  utop3cls  24299  prdsmet  24418  metustrel  24600  icccmplem2  24872  xrge0tsms  24883  cnmptre  24977  icchmeo  24991  bndth  25008  lebnumlem2  25012  cfilresi  25345  causs  25348  bcthlem5  25378  evthicc  25509  ovolficcss  25519  ovolmge0  25527  ovolgelb  25530  ovollb2lem  25538  ovollb2  25539  ovolunlem1a  25546  ovolunlem1  25547  ovoliunlem1  25552  ovoliunlem2  25553  ovoliun  25555  ovolscalem1  25563  ovolicc1  25566  ovolicc2lem4  25570  ovolicc2  25572  voliunlem2  25601  voliunlem3  25602  ioombl1lem2  25609  ioombl1lem4  25611  uniioovol  25629  uniiccvol  25630  uniioombllem1  25631  uniioombllem2  25633  uniioombllem3  25635  uniioombllem4  25636  uniioombllem6  25638  dyadmbllem  25649  dyadmbl  25650  volcn  25656  vitalilem4  25661  vitalilem5  25662  cnmbf  25709  i1fmul  25746  itg1addlem4  25749  itg2seq  25792  dvbssntr  25950  dvreslem  25959  dvcjbr  25999  dvferm1  26035  dvferm2  26037  cmvth  26041  dvlip  26043  lhop1lem  26063  lhop2  26065  lhop  26066  dvcnvrelem2  26068  dvcnvre  26069  dvfsumle  26071  dvfsumge  26072  dvfsumabs  26073  dvfsumlem2  26077  ftc1a  26087  ftc1lem3  26088  ftc1lem6  26091  itgsubstlem  26098  itgpowd  26100  mdegleb  26112  mdeglt  26113  mdegldg  26114  mdegxrcl  26115  mdegcl  26117  deg1mul3le  26165  ig1pdvds  26228  plyeq0lem  26258  aannenlem2  26381  aalioulem3  26386  taylf  26412  taylthlem2  26425  pserulm  26473  psercn2  26474  psercn  26477  reeff1olem  26497  efcvx  26500  loglesqrt  26814  rlimcnp  27018  xrlimcnp  27021  jensen  27041  wilthlem2  27121  vmadivsumb  27535  pntrsumo1  27617  pntlem3  27661  noseqrdgfn  28387  bdaypw2n0bndlem  28544  perpln2  28868  axcontlem10  29131  usgrexmplef  29417  dfpth2  29886  nmoxr  30926  nmooge0  30927  nmoolb  30931  nmoubi  30932  ubthlem1  31030  shmodi  31550  nmopxr  32026  nmfnxr  32039  nmoplb  32067  nmopub  32068  nmfnlb  32084  nmfnleub  32085  nmopun  32174  branmfn  32265  mdslj1i  32479  hatomistici  32522  xppreima2  32814  fsuppcurry1  32887  fsuppcurry2  32888  fpwrelmap  32896  infxrge0gelb  32929  gsumpart  33204  xrge0tsmsd  33214  pmtrcnel2  33231  cyc3genpm  33293  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  1fldgenq  33470  ssdifidllem  33604  ssmxidllem  33622  mplmulmvr  33797  zarcmplem  34139  metideq  34151  metider  34152  pstmfval  34154  esumgect  34348  esum2d  34351  sigaclci  34390  insiga  34395  omssubadd  34558  eulerpartlemgs2  34638  ballotlemsima  34774  signsply0  34806  iblidicc  34847  fsum2dsub  34862  reprsuc  34870  reprgt  34876  bnj1145  35249  bnj1137  35251  bnj1136  35253  resconn  35557  cvmliftlem8  35603  cvmlift3lem6  35635  mclsssvlem  35873  mclsind  35881  mclsppslem  35894  ivthALT  36656  neibastop1  36680  topjoin  36686  dfttc2g  36827  bj-imdirco  37643  ptrecube  38080  poimirlem6  38086  poimirlem15  38095  heicant  38115  mblfinlem2  38118  mblfinlem3  38119  mblfinlem4  38120  ismblfin  38121  itg2gt0cn  38135  ftc1cnnc  38152  ftc1anclem3  38155  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  areacirclem2  38169  areacirclem3  38170  areacirclem4  38171  totbndbnd  38249  prdsbnd  38253  heiborlem1  38271  rrnequiv  38295  reheibor  38299  iccbnd  38300  pmapssbaN  40345  2polssN  40500  paddunN  40512  poldmj1N  40513  ispsubcl2N  40532  psubclinN  40533  paddatclN  40534  poml4N  40538  diaglbN  41640  diaintclN  41643  dibglbN  41751  dibintclN  41752  dicssdvh  41771  dihvalrel  41864  dochexmidlem4  42048  infdesc  43186  ttac  43574  hbtlem6  43667  hbt  43668  cnvssb  44123  cnvrcl0  44162  cnvtrrel  44207  relexpaddss  44255  cotrcltrcl  44262  cotrclrcl  44279  frege96d  44286  frege97d  44289  frege109d  44294  frege131d  44301  rfovcnvf1od  44541  isotone2  44586  gneispace  44671  k0004ss1  44688  grumnudlem  44822  uzfissfz  45863  suplesup  45876  ssrexr  45967  limciccioolb  46158  limcicciooub  46172  limcleqr  46179  cnrefiisplem  46364  cncfiooicclem1  46428  ibliccsinexp  46486  iblioosinexp  46488  itgcoscmulx  46504  itgsincmulx  46509  itgsubsticclem  46510  itgiccshift  46515  itgperiod  46516  itgsbtaddcnst  46517  stoweidlem34  46569  stoweidlem59  46594  dirkeritg  46637  dirkercncflem2  46639  fourierdlem20  46662  fourierdlem31  46673  fourierdlem39  46681  fourierdlem42  46684  fourierdlem46  46687  fourierdlem52  46693  fourierdlem53  46694  fourierdlem60  46701  fourierdlem61  46702  fourierdlem62  46703  fourierdlem68  46709  fourierdlem76  46717  fourierdlem85  46726  fourierdlem88  46729  fourierdlem89  46730  fourierdlem90  46731  fourierdlem91  46732  fourierdlem93  46734  fourierdlem94  46735  fourierdlem103  46744  fourierdlem104  46745  fourierdlem111  46752  fouriersw  46766  etransclem46  46815  etransclem48  46817  sge0less  46927  sge0resplit  46941  sge0isum  46962  hoicvr  47083  pimdecfgtioo  47252  pimincfltioo  47253  iccpartipre  47988  bgoldbtbndlem2  48389  setrec1lem4  50272  setrec2fun  50274