Theorem sstrdi 3994

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

Syntax hints:   → wi 4   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  difss2  4133  rintn0  5112  eqbrrdva  5869  ssxpb  6173  resssxp  6269  relfld  6274  funssxp  6746  dff2  7100  dff3  7101  fliftf  7315  1stcof  8009  2ndcof  8010  frxp2  8135  frxp3  8142  frrlem13  8289  nnunifi  9300  elfiun  9431  marypha1lem  9434  marypha1  9435  ordtypelem7  9525  tcmin  9742  unwf  9811  rankfu  9878  tcrank  9885  aceq3lem  10121  dfac12lem2  10145  ackbij1lem9  10229  ackbij1lem10  10230  ackbij1lem16  10236  fin23lem26  10326  fin23lem27  10329  fin1a2lem6  10406  itunitc  10422  axdc3lem2  10452  ttukeylem5  10514  fpwwe2lem12  10643  canthwelem  10651  pwfseqlem4  10663  wunex2  10739  wunex3  10742  inar1  10776  inatsk  10779  gruina  10819  suprfinzcl  12683  suprzub  12930  uzsupss  12931  uzwo3  12934  rpnnen1lem4  12971  rpnnen1lem5  12972  supxrre  13313  infxrre  13322  ioodisj  13466  supicclub2  13488  fzssnn  13552  fzossnn0  13670  elfzom1elp1fzo  13706  injresinjlem  13759  uzindi  13954  ssnn0fi  13957  seqcoll  14432  seqcoll2  14433  reltrclfv  14971  relexpdmg  14996  relexpdm  14997  relexprng  15000  relexprn  15001  relexpfld  15003  relexpaddg  15007  limsupval2  15431  limsupgre  15432  limsupbnd2  15434  rlimuni  15501  rlimcld2  15529  rlimno1  15607  isercolllem2  15619  isercoll  15621  summolem2a  15668  summolem2  15669  fsumsers  15681  fsumcvg3  15682  prodmolem2a  15885  prodmolem2  15886  zprod  15888  lcmfnnval  16568  lcmfnncl  16573  4sqlem11  16895  vdwlem8  16928  vdwlem11  16931  ramub2  16954  0ram  16960  0ram2  16961  0ramcl  16963  ramub1lem2  16967  prmgaplem3  16993  prmgaplem4  16994  isohom  17730  funcres2c  17861  resscntz  19245  cntzidss  19252  cntzmhm2  19254  pgpssslw  19530  cntzspan  19760  gsumval3  19823  gsum2d  19888  dprdspan  19945  dprdres  19946  subdrgint  20650  sdrgint  20651  primefld  20652  lssintcl  20807  lbsextlem2  21006  lbsextlem3  21007  lbsextlem4  21008  islinds3  21699  fctop  22827  cctop  22829  neitr  23004  ordtbas2  23015  ordtopn1  23018  ordtopn2  23019  lmss  23122  clsconn  23254  2ndcdisj  23280  2ndcomap  23282  ptbasfi  23405  txcmplem2  23466  hausdiag  23469  txkgen  23476  basqtop  23535  alexsubb  23870  alexsubALTlem4  23874  tsmsres  23968  tsmsxplem1  23977  tsmsxp  23979  ustrel  24036  utop3cls  24076  prdsmet  24196  metustrel  24381  icccmplem2  24659  xrge0tsms  24670  cnmptre  24768  icchmeo  24785  icchmeoOLD  24786  bndth  24804  lebnumlem2  24808  cfilresi  25143  causs  25146  bcthlem5  25176  evthicc  25308  ovolficcss  25318  ovolmge0  25326  ovolgelb  25329  ovollb2lem  25337  ovollb2  25338  ovolunlem1a  25345  ovolunlem1  25346  ovoliunlem1  25351  ovoliunlem2  25352  ovoliun  25354  ovolscalem1  25362  ovolicc1  25365  ovolicc2lem4  25369  ovolicc2  25371  voliunlem2  25400  voliunlem3  25401  ioombl1lem2  25408  ioombl1lem4  25410  uniioovol  25428  uniiccvol  25429  uniioombllem1  25430  uniioombllem2  25432  uniioombllem3  25434  uniioombllem4  25435  uniioombllem6  25437  dyadmbllem  25448  dyadmbl  25449  volcn  25455  vitalilem4  25460  vitalilem5  25461  cnmbf  25508  i1fmul  25545  itg1addlem4  25548  itg1addlem4OLD  25549  itg2seq  25592  dvbssntr  25749  dvreslem  25758  dvcjbr  25801  dvferm1  25837  dvferm2  25839  cmvth  25843  cmvthOLD  25844  dvlip  25846  lhop1lem  25866  lhop2  25868  lhop  25869  dvcnvrelem2  25871  dvcnvre  25872  dvfsumle  25874  dvfsumleOLD  25875  dvfsumge  25876  dvfsumabs  25877  dvfsumlem2  25881  dvfsumlem2OLD  25882  ftc1a  25892  ftc1lem3  25893  ftc1lem6  25896  itgsubstlem  25903  itgpowd  25905  mdegleb  25920  mdeglt  25921  mdegldg  25922  mdegxrcl  25923  mdegcl  25925  deg1mul3le  25972  ig1pdvds  26032  plyeq0lem  26062  aannenlem2  26181  aalioulem3  26186  taylf  26212  taylthlem2  26225  pserulm  26273  psercn2  26274  psercn2OLD  26275  psercn  26278  reeff1olem  26298  efcvx  26301  loglesqrt  26607  rlimcnp  26811  xrlimcnp  26814  jensen  26834  wilthlem2  26914  vmadivsumb  27329  pntrsumo1  27411  pntlem3  27455  perpln2  28395  axcontlem10  28664  usgrexmplef  28949  nmoxr  30452  nmooge0  30453  nmoolb  30457  nmoubi  30458  ubthlem1  30556  shmodi  31076  nmopxr  31552  nmfnxr  31565  nmoplb  31593  nmopub  31594  nmfnlb  31610  nmfnleub  31611  nmopun  31700  branmfn  31791  mdslj1i  32005  hatomistici  32048  xppreima2  32309  fsuppcurry1  32383  fsuppcurry2  32384  fpwrelmap  32391  infxrge0gelb  32412  prmdvdsbc  32455  gsumpart  32643  xrge0tsmsd  32645  pmtrcnel2  32687  cyc3genpm  32747  1fldgenq  32848  ssmxidllem  33029  zarcmplem  33325  metideq  33337  metider  33338  pstmfval  33340  esumgect  33552  esum2d  33555  sigaclci  33594  insiga  33599  omssubadd  33763  eulerpartlemgs2  33843  ballotlemsima  33978  signsply0  34026  iblidicc  34068  fsum2dsub  34083  reprsuc  34091  reprgt  34097  bnj1145  34468  bnj1137  34470  bnj1136  34472  resconn  34701  cvmliftlem8  34747  cvmlift3lem6  34779  mclsssvlem  35017  mclsind  35025  mclsppslem  35038  ivthALT  35684  neibastop1  35708  topjoin  35714  bj-imdirco  36535  ptrecube  36952  poimirlem6  36958  poimirlem15  36967  heicant  36987  mblfinlem2  36990  mblfinlem3  36991  mblfinlem4  36992  ismblfin  36993  itg2gt0cn  37007  ftc1cnnc  37024  ftc1anclem3  37027  ftc1anclem7  37031  ftc1anclem8  37032  ftc1anc  37033  areacirclem2  37041  areacirclem3  37042  areacirclem4  37043  totbndbnd  37121  prdsbnd  37125  heiborlem1  37143  rrnequiv  37167  reheibor  37171  iccbnd  37172  pmapssbaN  39095  2polssN  39250  paddunN  39262  poldmj1N  39263  ispsubcl2N  39282  psubclinN  39283  paddatclN  39284  poml4N  39288  diaglbN  40390  diaintclN  40393  dibglbN  40501  dibintclN  40502  dicssdvh  40521  dihvalrel  40614  dochexmidlem4  40798  infdesc  41848  rmxyelqirrOLD  42112  ttac  42238  hbtlem6  42334  hbt  42335  cnvssb  42800  cnvrcl0  42839  cnvtrrel  42884  relexpaddss  42932  cotrcltrcl  42939  cotrclrcl  42956  frege96d  42963  frege97d  42966  frege109d  42971  frege131d  42978  rfovcnvf1od  43218  isotone2  43263  gneispace  43348  k0004ss1  43365  grumnudlem  43507  uzfissfz  44495  suplesup  44508  ssrexr  44601  limciccioolb  44796  limcicciooub  44812  limcleqr  44819  cnrefiisplem  45004  cncfiooicclem1  45068  ibliccsinexp  45126  iblioosinexp  45128  itgcoscmulx  45144  itgsincmulx  45149  itgsubsticclem  45150  itgiccshift  45155  itgperiod  45156  itgsbtaddcnst  45157  stoweidlem34  45209  stoweidlem59  45234  dirkeritg  45277  dirkercncflem2  45279  fourierdlem20  45302  fourierdlem31  45313  fourierdlem39  45321  fourierdlem42  45324  fourierdlem46  45327  fourierdlem52  45333  fourierdlem53  45334  fourierdlem60  45341  fourierdlem61  45342  fourierdlem62  45343  fourierdlem68  45349  fourierdlem76  45357  fourierdlem85  45366  fourierdlem88  45369  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  fourierdlem93  45374  fourierdlem94  45375  fourierdlem103  45384  fourierdlem104  45385  fourierdlem111  45392  fouriersw  45406  etransclem46  45455  etransclem48  45457  sge0less  45567  sge0resplit  45581  sge0isum  45602  pimdecfgtioo  45892  pimincfltioo  45893  iccpartipre  46548  bgoldbtbndlem2  46933  setrec1lem4  47897  setrec2fun  47899