Theorem sstrdi 3992

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

Syntax hints:   → wi 4   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  difss2  4132  rintn0  5112  eqbrrdva  5872  ssxpb  6178  resssxp  6274  relfld  6279  funssxp  6752  dff2  7109  dff3  7110  fliftf  7323  1stcof  8023  2ndcof  8024  frxp2  8149  frxp3  8156  frrlem13  8303  nnunifi  9318  elfiun  9453  marypha1lem  9456  marypha1  9457  ordtypelem7  9547  tcmin  9764  unwf  9833  rankfu  9900  tcrank  9907  aceq3lem  10143  dfac12lem2  10167  ackbij1lem9  10251  ackbij1lem10  10252  ackbij1lem16  10258  fin23lem26  10348  fin23lem27  10351  fin1a2lem6  10428  itunitc  10444  axdc3lem2  10474  ttukeylem5  10536  fpwwe2lem12  10665  canthwelem  10673  pwfseqlem4  10685  wunex2  10761  wunex3  10764  inar1  10798  inatsk  10801  gruina  10841  suprfinzcl  12706  suprzub  12953  uzsupss  12954  uzwo3  12957  rpnnen1lem4  12994  rpnnen1lem5  12995  supxrre  13338  infxrre  13347  ioodisj  13491  supicclub2  13513  fzssnn  13577  fzossnn0  13695  elfzom1elp1fzo  13731  injresinjlem  13784  uzindi  13979  ssnn0fi  13982  seqcoll  14457  seqcoll2  14458  reltrclfv  14996  relexpdmg  15021  relexpdm  15022  relexprng  15025  relexprn  15026  relexpfld  15028  relexpaddg  15032  limsupval2  15456  limsupgre  15457  limsupbnd2  15459  rlimuni  15526  rlimcld2  15554  rlimno1  15632  isercolllem2  15644  isercoll  15646  summolem2a  15693  summolem2  15694  fsumsers  15706  fsumcvg3  15707  prodmolem2a  15910  prodmolem2  15911  zprod  15913  lcmfnnval  16594  lcmfnncl  16599  prmdvdsbc  16697  4sqlem11  16923  vdwlem8  16956  vdwlem11  16959  ramub2  16982  0ram  16988  0ram2  16989  0ramcl  16991  ramub1lem2  16995  prmgaplem3  17021  prmgaplem4  17022  isohom  17758  funcres2c  17889  resscntz  19283  cntzidss  19290  cntzmhm2  19292  pgpssslw  19568  cntzspan  19798  gsumval3  19861  gsum2d  19926  dprdspan  19983  dprdres  19984  subdrgint  20690  sdrgint  20691  primefld  20692  lssintcl  20847  lbsextlem2  21046  lbsextlem3  21047  lbsextlem4  21048  islinds3  21767  fctop  22906  cctop  22908  neitr  23083  ordtbas2  23094  ordtopn1  23097  ordtopn2  23098  lmss  23201  clsconn  23333  2ndcdisj  23359  2ndcomap  23361  ptbasfi  23484  txcmplem2  23545  hausdiag  23548  txkgen  23555  basqtop  23614  alexsubb  23949  alexsubALTlem4  23953  tsmsres  24047  tsmsxplem1  24056  tsmsxp  24058  ustrel  24115  utop3cls  24155  prdsmet  24275  metustrel  24460  icccmplem2  24738  xrge0tsms  24749  cnmptre  24847  icchmeo  24864  icchmeoOLD  24865  bndth  24883  lebnumlem2  24887  cfilresi  25222  causs  25225  bcthlem5  25255  evthicc  25387  ovolficcss  25397  ovolmge0  25405  ovolgelb  25408  ovollb2lem  25416  ovollb2  25417  ovolunlem1a  25424  ovolunlem1  25425  ovoliunlem1  25430  ovoliunlem2  25431  ovoliun  25433  ovolscalem1  25441  ovolicc1  25444  ovolicc2lem4  25448  ovolicc2  25450  voliunlem2  25479  voliunlem3  25480  ioombl1lem2  25487  ioombl1lem4  25489  uniioovol  25507  uniiccvol  25508  uniioombllem1  25509  uniioombllem2  25511  uniioombllem3  25513  uniioombllem4  25514  uniioombllem6  25516  dyadmbllem  25527  dyadmbl  25528  volcn  25534  vitalilem4  25539  vitalilem5  25540  cnmbf  25587  i1fmul  25624  itg1addlem4  25627  itg1addlem4OLD  25628  itg2seq  25671  dvbssntr  25828  dvreslem  25837  dvcjbr  25880  dvferm1  25916  dvferm2  25918  cmvth  25922  cmvthOLD  25923  dvlip  25925  lhop1lem  25945  lhop2  25947  lhop  25948  dvcnvrelem2  25950  dvcnvre  25951  dvfsumle  25953  dvfsumleOLD  25954  dvfsumge  25955  dvfsumabs  25956  dvfsumlem2  25960  dvfsumlem2OLD  25961  ftc1a  25971  ftc1lem3  25972  ftc1lem6  25975  itgsubstlem  25982  itgpowd  25984  mdegleb  25999  mdeglt  26000  mdegldg  26001  mdegxrcl  26002  mdegcl  26004  deg1mul3le  26051  ig1pdvds  26113  plyeq0lem  26143  aannenlem2  26263  aalioulem3  26268  taylf  26294  taylthlem2  26308  taylthlem2OLD  26309  pserulm  26357  psercn2  26358  psercn2OLD  26359  psercn  26362  reeff1olem  26382  efcvx  26385  loglesqrt  26692  rlimcnp  26896  xrlimcnp  26899  jensen  26920  wilthlem2  27000  vmadivsumb  27415  pntrsumo1  27497  pntlem3  27541  noseqrdgfn  28178  perpln2  28514  axcontlem10  28783  usgrexmplef  29071  nmoxr  30575  nmooge0  30576  nmoolb  30580  nmoubi  30581  ubthlem1  30679  shmodi  31199  nmopxr  31675  nmfnxr  31688  nmoplb  31716  nmopub  31717  nmfnlb  31733  nmfnleub  31734  nmopun  31823  branmfn  31914  mdslj1i  32128  hatomistici  32171  xppreima2  32436  fsuppcurry1  32507  fsuppcurry2  32508  fpwrelmap  32515  infxrge0gelb  32536  gsumpart  32769  xrge0tsmsd  32771  pmtrcnel2  32813  cyc3genpm  32873  1fldgenq  33009  ssmxidllem  33186  zarcmplem  33482  metideq  33494  metider  33495  pstmfval  33497  esumgect  33709  esum2d  33712  sigaclci  33751  insiga  33756  omssubadd  33920  eulerpartlemgs2  34000  ballotlemsima  34135  signsply0  34183  iblidicc  34224  fsum2dsub  34239  reprsuc  34247  reprgt  34253  bnj1145  34624  bnj1137  34626  bnj1136  34628  resconn  34856  cvmliftlem8  34902  cvmlift3lem6  34934  mclsssvlem  35172  mclsind  35180  mclsppslem  35193  ivthALT  35819  neibastop1  35843  topjoin  35849  bj-imdirco  36669  ptrecube  37093  poimirlem6  37099  poimirlem15  37108  heicant  37128  mblfinlem2  37131  mblfinlem3  37132  mblfinlem4  37133  ismblfin  37134  itg2gt0cn  37148  ftc1cnnc  37165  ftc1anclem3  37168  ftc1anclem7  37172  ftc1anclem8  37173  ftc1anc  37174  areacirclem2  37182  areacirclem3  37183  areacirclem4  37184  totbndbnd  37262  prdsbnd  37266  heiborlem1  37284  rrnequiv  37308  reheibor  37312  iccbnd  37313  pmapssbaN  39233  2polssN  39388  paddunN  39400  poldmj1N  39401  ispsubcl2N  39420  psubclinN  39421  paddatclN  39422  poml4N  39426  diaglbN  40528  diaintclN  40531  dibglbN  40639  dibintclN  40640  dicssdvh  40659  dihvalrel  40752  dochexmidlem4  40936  infdesc  42067  rmxyelqirrOLD  42331  ttac  42457  hbtlem6  42553  hbt  42554  cnvssb  43016  cnvrcl0  43055  cnvtrrel  43100  relexpaddss  43148  cotrcltrcl  43155  cotrclrcl  43172  frege96d  43179  frege97d  43182  frege109d  43187  frege131d  43194  rfovcnvf1od  43434  isotone2  43479  gneispace  43564  k0004ss1  43581  grumnudlem  43722  uzfissfz  44708  suplesup  44721  ssrexr  44814  limciccioolb  45009  limcicciooub  45025  limcleqr  45032  cnrefiisplem  45217  cncfiooicclem1  45281  ibliccsinexp  45339  iblioosinexp  45341  itgcoscmulx  45357  itgsincmulx  45362  itgsubsticclem  45363  itgiccshift  45368  itgperiod  45369  itgsbtaddcnst  45370  stoweidlem34  45422  stoweidlem59  45447  dirkeritg  45490  dirkercncflem2  45492  fourierdlem20  45515  fourierdlem31  45526  fourierdlem39  45534  fourierdlem42  45537  fourierdlem46  45540  fourierdlem52  45546  fourierdlem53  45547  fourierdlem60  45554  fourierdlem61  45555  fourierdlem62  45556  fourierdlem68  45562  fourierdlem76  45570  fourierdlem85  45579  fourierdlem88  45582  fourierdlem89  45583  fourierdlem90  45584  fourierdlem91  45585  fourierdlem93  45587  fourierdlem94  45588  fourierdlem103  45597  fourierdlem104  45598  fourierdlem111  45605  fouriersw  45619  etransclem46  45668  etransclem48  45670  sge0less  45780  sge0resplit  45794  sge0isum  45815  pimdecfgtioo  46105  pimincfltioo  46106  iccpartipre  46761  bgoldbtbndlem2  47146  setrec1lem4  48121  setrec2fun  48123