Theorem sstrdi 3995

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

Syntax hints:   → wi 4   ⊆ wss 3950

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

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

This theorem is referenced by:  difss2  4137  rintn0  5108  eqbrrdva  5879  ssxpb  6193  resssxp  6289  relfld  6294  funssxp  6763  dff2  7118  dff3  7119  fliftf  7336  1stcof  8045  2ndcof  8046  frxp2  8170  frxp3  8177  frrlem13  8324  nnunifi  9328  elfiun  9471  marypha1lem  9474  marypha1  9475  ordtypelem7  9565  tcmin  9782  unwf  9851  rankfu  9918  tcrank  9925  aceq3lem  10161  dfac12lem2  10186  ackbij1lem9  10268  ackbij1lem10  10269  ackbij1lem16  10275  fin23lem26  10366  fin23lem27  10369  fin1a2lem6  10446  itunitc  10462  axdc3lem2  10492  ttukeylem5  10554  fpwwe2lem12  10683  canthwelem  10691  pwfseqlem4  10703  wunex2  10779  wunex3  10782  inar1  10816  inatsk  10819  gruina  10859  suprfinzcl  12734  suprzub  12982  uzsupss  12983  uzwo3  12986  rpnnen1lem4  13023  rpnnen1lem5  13024  supxrre  13370  infxrre  13379  ioodisj  13523  supicclub2  13545  fzssnn  13609  fzossnn0  13731  elfzom1elp1fzo  13772  injresinjlem  13827  uzindi  14024  ssnn0fi  14027  seqcoll  14504  seqcoll2  14505  reltrclfv  15057  relexpdmg  15082  relexpdm  15083  relexprng  15086  relexprn  15087  relexpfld  15089  relexpaddg  15093  limsupval2  15517  limsupgre  15518  limsupbnd2  15520  rlimuni  15587  rlimcld2  15615  rlimno1  15691  isercolllem2  15703  isercoll  15705  summolem2a  15752  summolem2  15753  fsumsers  15765  fsumcvg3  15766  prodmolem2a  15971  prodmolem2  15972  zprod  15974  lcmfnnval  16662  lcmfnncl  16667  prmdvdsbc  16764  4sqlem11  16994  vdwlem8  17027  vdwlem11  17030  ramub2  17053  0ram  17059  0ram2  17060  0ramcl  17062  ramub1lem2  17066  prmgaplem3  17092  prmgaplem4  17093  isohom  17821  funcres2c  17949  resscntz  19352  cntzidss  19359  cntzmhm2  19361  pgpssslw  19633  cntzspan  19863  gsumval3  19926  gsum2d  19991  dprdspan  20048  dprdres  20049  subdrgint  20805  sdrgint  20806  primefld  20807  lssintcl  20963  lbsextlem2  21162  lbsextlem3  21163  lbsextlem4  21164  islinds3  21855  fctop  23012  cctop  23014  neitr  23189  ordtbas2  23200  ordtopn1  23203  ordtopn2  23204  lmss  23307  clsconn  23439  2ndcdisj  23465  2ndcomap  23467  ptbasfi  23590  txcmplem2  23651  hausdiag  23654  txkgen  23661  basqtop  23720  alexsubb  24055  alexsubALTlem4  24059  tsmsres  24153  tsmsxplem1  24162  tsmsxp  24164  ustrel  24221  utop3cls  24261  prdsmet  24381  metustrel  24566  icccmplem2  24846  xrge0tsms  24857  cnmptre  24955  icchmeo  24972  icchmeoOLD  24973  bndth  24991  lebnumlem2  24995  cfilresi  25330  causs  25333  bcthlem5  25363  evthicc  25495  ovolficcss  25505  ovolmge0  25513  ovolgelb  25516  ovollb2lem  25524  ovollb2  25525  ovolunlem1a  25532  ovolunlem1  25533  ovoliunlem1  25538  ovoliunlem2  25539  ovoliun  25541  ovolscalem1  25549  ovolicc1  25552  ovolicc2lem4  25556  ovolicc2  25558  voliunlem2  25587  voliunlem3  25588  ioombl1lem2  25595  ioombl1lem4  25597  uniioovol  25615  uniiccvol  25616  uniioombllem1  25617  uniioombllem2  25619  uniioombllem3  25621  uniioombllem4  25622  uniioombllem6  25624  dyadmbllem  25635  dyadmbl  25636  volcn  25642  vitalilem4  25647  vitalilem5  25648  cnmbf  25695  i1fmul  25732  itg1addlem4  25735  itg2seq  25778  dvbssntr  25936  dvreslem  25945  dvcjbr  25988  dvferm1  26024  dvferm2  26026  cmvth  26030  cmvthOLD  26031  dvlip  26033  lhop1lem  26053  lhop2  26055  lhop  26056  dvcnvrelem2  26058  dvcnvre  26059  dvfsumle  26061  dvfsumleOLD  26062  dvfsumge  26063  dvfsumabs  26064  dvfsumlem2  26068  dvfsumlem2OLD  26069  ftc1a  26079  ftc1lem3  26080  ftc1lem6  26083  itgsubstlem  26090  itgpowd  26092  mdegleb  26104  mdeglt  26105  mdegldg  26106  mdegxrcl  26107  mdegcl  26109  deg1mul3le  26157  ig1pdvds  26220  plyeq0lem  26250  aannenlem2  26372  aalioulem3  26377  taylf  26403  taylthlem2  26417  taylthlem2OLD  26418  pserulm  26466  psercn2  26467  psercn2OLD  26468  psercn  26471  reeff1olem  26491  efcvx  26494  loglesqrt  26805  rlimcnp  27009  xrlimcnp  27012  jensen  27033  wilthlem2  27113  vmadivsumb  27528  pntrsumo1  27610  pntlem3  27654  noseqrdgfn  28313  perpln2  28720  axcontlem10  28989  usgrexmplef  29277  dfpth2  29750  nmoxr  30786  nmooge0  30787  nmoolb  30791  nmoubi  30792  ubthlem1  30890  shmodi  31410  nmopxr  31886  nmfnxr  31899  nmoplb  31927  nmopub  31928  nmfnlb  31944  nmfnleub  31945  nmopun  32034  branmfn  32125  mdslj1i  32339  hatomistici  32382  xppreima2  32662  fsuppcurry1  32737  fsuppcurry2  32738  fpwrelmap  32745  infxrge0gelb  32771  gsumpart  33061  xrge0tsmsd  33066  pmtrcnel2  33111  cyc3genpm  33173  elrgspnsubrunlem1  33252  elrgspnsubrunlem2  33253  1fldgenq  33325  ssdifidllem  33485  ssmxidllem  33502  zarcmplem  33881  metideq  33893  metider  33894  pstmfval  33896  esumgect  34092  esum2d  34095  sigaclci  34134  insiga  34139  omssubadd  34303  eulerpartlemgs2  34383  ballotlemsima  34519  signsply0  34567  iblidicc  34608  fsum2dsub  34623  reprsuc  34631  reprgt  34637  bnj1145  35008  bnj1137  35010  bnj1136  35012  resconn  35252  cvmliftlem8  35298  cvmlift3lem6  35330  mclsssvlem  35568  mclsind  35576  mclsppslem  35589  ivthALT  36337  neibastop1  36361  topjoin  36367  bj-imdirco  37192  ptrecube  37628  poimirlem6  37634  poimirlem15  37643  heicant  37663  mblfinlem2  37666  mblfinlem3  37667  mblfinlem4  37668  ismblfin  37669  itg2gt0cn  37683  ftc1cnnc  37700  ftc1anclem3  37703  ftc1anclem7  37707  ftc1anclem8  37708  ftc1anc  37709  areacirclem2  37717  areacirclem3  37718  areacirclem4  37719  totbndbnd  37797  prdsbnd  37801  heiborlem1  37819  rrnequiv  37843  reheibor  37847  iccbnd  37848  pmapssbaN  39763  2polssN  39918  paddunN  39930  poldmj1N  39931  ispsubcl2N  39950  psubclinN  39951  paddatclN  39952  poml4N  39956  diaglbN  41058  diaintclN  41061  dibglbN  41169  dibintclN  41170  dicssdvh  41189  dihvalrel  41282  dochexmidlem4  41466  infdesc  42658  rmxyelqirrOLD  42927  ttac  43053  hbtlem6  43146  hbt  43147  cnvssb  43604  cnvrcl0  43643  cnvtrrel  43688  relexpaddss  43736  cotrcltrcl  43743  cotrclrcl  43760  frege96d  43767  frege97d  43770  frege109d  43775  frege131d  43782  rfovcnvf1od  44022  isotone2  44067  gneispace  44152  k0004ss1  44169  grumnudlem  44309  uzfissfz  45342  suplesup  45355  ssrexr  45448  limciccioolb  45641  limcicciooub  45657  limcleqr  45664  cnrefiisplem  45849  cncfiooicclem1  45913  ibliccsinexp  45971  iblioosinexp  45973  itgcoscmulx  45989  itgsincmulx  45994  itgsubsticclem  45995  itgiccshift  46000  itgperiod  46001  itgsbtaddcnst  46002  stoweidlem34  46054  stoweidlem59  46079  dirkeritg  46122  dirkercncflem2  46124  fourierdlem20  46147  fourierdlem31  46158  fourierdlem39  46166  fourierdlem42  46169  fourierdlem46  46172  fourierdlem52  46178  fourierdlem53  46179  fourierdlem60  46186  fourierdlem61  46187  fourierdlem62  46188  fourierdlem68  46194  fourierdlem76  46202  fourierdlem85  46211  fourierdlem88  46214  fourierdlem89  46215  fourierdlem90  46216  fourierdlem91  46217  fourierdlem93  46219  fourierdlem94  46220  fourierdlem103  46229  fourierdlem104  46230  fourierdlem111  46237  fouriersw  46251  etransclem46  46300  etransclem48  46302  sge0less  46412  sge0resplit  46426  sge0isum  46447  pimdecfgtioo  46737  pimincfltioo  46738  iccpartipre  47413  bgoldbtbndlem2  47798  setrec1lem4  49264  setrec2fun  49266