Theorem sstrid 3933

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)

Hypotheses

Ref	Expression
sstrid.1	⊢ 𝐴 ⊆ 𝐵
sstrid.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
sstrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrid

Step	Hyp	Ref	Expression
1		sstrid.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3		sstrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	sstrd 3932	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  difsymssdifssd  4188  wereu2  5587  sofld  6095  resssxp  6177  frpomin  6247  fimass  6630  fvmptss  6896  fimacnvOLD  6957  isofr2  7224  frxp  7976  fnse  7983  frrlem4  8114  frrlem13  8123  fprlem1  8125  smores2  8194  dffi3  9199  marypha1lem  9201  ordtypelem7  9292  ordtypelem8  9293  oismo  9308  unxpwdom2  9356  cantnfres  9444  oemapvali  9451  frmin  9516  frrlem15  9524  frrlem16  9525  tskwe  9717  acndom2  9819  dfac2a  9894  dfac12lem2  9909  cfle  10019  cofsmo  10034  coftr  10038  isf34lem5  10143  isf34lem7  10144  isf34lem6  10145  enfin1ai  10149  fin1a2lem12  10176  ttukeylem7  10280  alephexp1  10344  fpwwe2lem12  10407  fpwwe2  10408  canth4  10412  canthwelem  10415  pwfseqlem1  10423  pwfseqlem4  10427  fzossnn0  13427  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  xptrrel  14700  limsupgle  15195  limsupgre  15199  rlimres  15276  lo1res  15277  lo1resb  15282  rlimresb  15283  o1resb  15284  o1of2  15331  o1rlimmul  15337  isercolllem2  15386  isercoll  15388  climsup  15390  fprodntriv  15661  bitsinvp1  16165  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadasslem  16186  sadeq  16188  bitsres  16189  smuval2  16198  smupval  16204  smueqlem  16206  smumul  16209  1arith  16637  isstruct2  16859  setscom  16890  ressress  16967  imasvscafn  17257  imasless  17260  mrcssv  17332  isacs1i  17375  mreacs  17376  acsfn  17377  isacs4lem  18271  isacs5lem  18272  mhmima  18472  cntzmhm  18954  f1omvdconj  19063  f1omvdco2  19065  symgsssg  19084  symggen  19087  efgval  19332  gsumzaddlem  19531  gsumconst  19544  dmdprdd  19611  dprdfeq0  19634  dprdres  19640  dprdss  19641  dprdz  19642  subgdmdprd  19646  dprddisj2  19651  dprd2dlem1  19653  dprd2da  19654  dprd2d2  19656  dmdprdsplit2lem  19657  lmhmlsp  20320  lsppratlem4  20421  islbs3  20426  lbsextlem3  20431  znleval  20771  evpmss  20800  frlmsslsp  21012  lindff1  21036  lindfrn  21037  f1lindf  21038  lindfmm  21043  lsslindf  21046  mplcoe5  21250  mplind  21287  basdif0  22112  tgcl  22128  ppttop  22166  epttop  22168  ntrin  22221  mretopd  22252  neiptoptop  22291  cnclsi  22432  cnconst2  22443  cnrest2  22446  cnpresti  22448  cnprest2  22450  fiuncmp  22564  connsub  22581  connima  22585  iunconnlem  22587  1stcfb  22605  2ndc1stc  22611  2ndcdisj  22616  kgentopon  22698  llycmpkgen2  22710  1stckgenlem  22713  kgencn3  22718  ptclsg  22775  ptcnplem  22781  txtube  22800  hausdiag  22805  txkgen  22812  xkoco1cn  22817  xkoco2cn  22818  xkococnlem  22819  qtoptop2  22859  basqtop  22871  imastopn  22880  hmeores  22931  hmphdis  22956  ptcmpfi  22973  fbssfi  22997  filin  23014  infil  23023  fgtr  23050  elfm  23107  hausflim  23141  flimclslem  23144  fclscmp  23190  cnextcn  23227  tmdgsum2  23256  tgpconncomp  23273  ustexsym  23376  ustund  23382  ustimasn  23389  utoptop  23395  utopbas  23396  restutopopn  23399  blin2  23591  metustexhalf  23721  icccmplem2  23995  icccmplem3  23996  reconnlem2  23999  tcphcph  24410  fmcfil  24445  resscdrg  24531  ivthlem2  24625  ivthlem3  24626  ivth2  24628  ovolfiniun  24674  ovoliunlem1  24675  ismbl2  24700  nulmbl2  24709  unmbl  24710  shftmbl  24711  voliunlem1  24723  voliunlem2  24724  ioombl1lem4  24734  uniioombllem4  24759  uniioombllem5  24760  dyadmbllem  24772  dyadmbl  24773  mbflimsup  24839  i1fima  24851  i1fima2  24852  i1fadd  24868  itg1addlem4  24872  itg1addlem4OLD  24873  itg2splitlem  24922  itg2split  24923  ellimc3  25052  limcflflem  25053  limcflf  25054  limcresi  25058  limciun  25067  dvreslem  25082  dvres2lem  25083  dvres  25084  dvaddbr  25111  dvmulbr  25112  dvlip  25166  dvlip2  25168  c1liplem1  25169  dvivthlem1  25181  dvne0  25184  lhop1lem  25186  lhop  25189  dvcnvrelem1  25190  dvcnvrelem2  25191  dvfsumle  25194  dvfsumabs  25196  dvfsumlem2  25200  itgsubstlem  25221  mdegleb  25238  mdeglt  25239  mdegldg  25240  mdegxrcl  25241  mdegcl  25243  ig1peu  25345  reeff1olem  25614  logccv  25827  rlimcnp2  26125  lgamgulmlem2  26188  ppisval  26262  prmdvdsfi  26265  mumul  26339  sqff1o  26340  chtlepsi  26363  chpub  26377  dchrisum0lem2a  26674  pntlem3  26766  ex-res  28814  htthlem  29288  chlejb1i  29847  ssmd2  30683  fz2ssnn0  31115  gsumpart  31324  gsumhashmul  31325  gsumle  31359  locfinreflem  31799  sibfof  32316  sitgclbn  32319  sitgaddlemb  32324  eulerpartlemgu  32353  ballotlemsima  32491  reprinrn  32607  bnj1311  33013  fnrelpredd  33070  erdsze2lem2  33175  iccllysconn  33221  cvmopnlem  33249  msrf  33513  frxp2  33800  frxp3  33806  nosupno  33915  noetalem1  33953  neiin  34530  neibastop1  34557  neibastop2lem  34558  topmeet  34562  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem19  35805  poimirlem30  35816  cnambfre  35834  itg2gt0cn  35841  sstotbnd2  35941  sstotbnd3  35943  ssbnd  35955  ismtyima  35970  heibor1lem  35976  idresssidinxp  36451  pmodlem2  37868  pmodN  37871  diaintclN  39079  djaclN  39157  dibintclN  39188  dicval  39197  dihoml4c  39397  djhcl  39421  infdesc  40487  isnacs2  40535  isnacs3  40539  diophrw  40588  pellfundre  40710  pellfundge  40711  pellfundlb  40713  pellfundglb  40714  fnwe2lem2  40883  lmhmfgima  40916  hbt  40962  cnvtrcl0  41241  trclrelexplem  41326  relexp0a  41331  isotone2  41666  imo72b2lem1  41787  climinf  43154  islptre  43167  limccog  43168  limcleqr  43192  itgcoscmulx  43517  ismbl3  43534  ismbl4  43541  stoweidlem27  43575  dirkercncflem2  43652  fourierdlem38  43693  fourierdlem49  43703  fourierdlem51  43705  fourierdlem54  43708  fourierdlem63  43717  fourierdlem68  43722  fourierdlem69  43723  fourierdlem70  43724  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem84  43738  fourierdlem85  43739  fourierdlem88  43742  fourierdlem100  43754  fourierdlem101  43755  fourierdlem104  43758  fourierdlem107  43761  fourierdlem111  43765  fourierdlem112  43766  caragenel2d  44077  hoidmv1lelem3  44138  hspmbllem3  44173  sssmf  44283  smfrec  44334  smfsuplem1  44355  mgmhmima  45367