Theorem sstrid 3951

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3925

This theorem is used by:  difsymssdifssd  4220  wereu2  5663  sofld  6190  resssxp  6277  frpomin  6348  fimass  6733  fvmptss  7009  isofr2  7353  frxp  8131  fnse  8138  frxp2  8149  frxp3  8156  frrlem4  8295  frrlem13  8304  fprlem1  8306  smores2  8350  naddunif  8689  dffi3  9401  marypha1lem  9403  ordtypelem7  9496  ordtypelem8  9497  oismo  9512  unxpwdom2  9560  cantnfres  9656  oemapvali  9663  frmin  9731  frrlem15  9739  frrlem16  9740  tskwe  9955  acndom2  10057  dfac2a  10132  dfac12lem2  10147  cfle  10255  cofsmo  10271  coftr  10275  isf34lem5  10380  isf34lem7  10381  isf34lem6  10382  enfin1ai  10386  fin1a2lem12  10413  ttukeylem7  10517  alephexp1  10582  fpwwe2lem12  10645  fpwwe2  10646  canth4  10650  canthwelem  10653  pwfseqlem1  10661  pwfseqlem4  10665  fzossnn0  13738  fsuppmapnn0fiublem  14046  fsuppmapnn0fiub  14047  xptrrel  15043  limsupgle  15554  limsupgre  15558  rlimres  15635  lo1res  15636  lo1resb  15641  rlimresb  15642  o1resb  15643  o1of2  15690  o1rlimmul  15696  isercolllem2  15743  isercoll  15745  climsup  15747  fprodntriv  16022  bitsinvp1  16532  sadcaddlem  16540  sadadd2lem  16542  sadadd3  16544  sadasslem  16553  sadeq  16555  bitsres  16556  smuval2  16565  smupval  16571  smueqlem  16573  smumul  16576  1arith  17012  isstruct2  17234  setscom  17265  ressress  17332  imasvscafn  17616  imasless  17619  mrcssv  17695  isacs1i  17738  mreacs  17739  acsfn  17740  isacs4lem  18625  isacs5lem  18626  mgmhmima  18802  mhmima  18915  cntzmhm  19442  f1omvdconj  19547  f1omvdco2  19549  symgsssg  19568  symggen  19571  efgval  19818  gsumzaddlem  20022  gsumconst  20035  dmdprdd  20102  dprdfeq0  20125  dprdres  20131  dprdss  20132  dprdz  20133  subgdmdprd  20137  dprddisj2  20142  dprd2dlem1  20144  dprd2da  20145  dprd2d2  20147  dmdprdsplit2lem  20148  gsumle  20246  lmhmlsp  21207  lsppratlem4  21311  islbs3  21316  lbsextlem3  21321  znleval  21741  evpmss  21773  frlmsslsp  21983  lindff1  22007  lindfrn  22008  f1lindf  22009  lindfmm  22014  lsslindf  22017  mplcoe5  22228  mplind  22258  basdif0  23147  tgcl  23163  ppttop  23201  epttop  23203  ntrin  23255  mretopd  23286  neiptoptop  23325  cnclsi  23466  cnconst2  23477  cnrest2  23480  cnpresti  23482  cnprest2  23484  fiuncmp  23598  connsub  23615  connima  23619  iunconnlem  23621  1stcfb  23639  2ndc1stc  23645  2ndcdisj  23650  kgentopon  23732  llycmpkgen2  23744  1stckgenlem  23747  kgencn3  23752  ptclsg  23809  ptcnplem  23815  txtube  23834  hausdiag  23839  txkgen  23846  xkoco1cn  23851  xkoco2cn  23852  xkococnlem  23853  qtoptop2  23893  basqtop  23905  imastopn  23914  hmeores  23965  hmphdis  23990  ptcmpfi  24007  fbssfi  24031  filin  24048  infil  24057  fgtr  24084  elfm  24141  hausflim  24175  flimclslem  24178  fclscmp  24224  cnextcn  24261  tmdgsum2  24290  tgpconncomp  24307  ustexsym  24410  ustund  24416  ustimasn  24422  utoptop  24428  utopbas  24429  restutopopn  24432  blin2  24623  metustexhalf  24750  icccmplem2  25018  icccmplem3  25019  reconnlem2  25022  tcphcph  25433  fmcfil  25468  resscdrg  25554  ivthlem2  25648  ivthlem3  25649  ivth2  25651  ovolfiniun  25697  ovoliunlem1  25698  ismbl2  25723  nulmbl2  25732  unmbl  25733  shftmbl  25734  voliunlem1  25746  voliunlem2  25747  ioombl1lem4  25757  uniioombllem4  25782  uniioombllem5  25783  dyadmbllem  25795  dyadmbl  25796  mbflimsup  25862  i1fima  25874  i1fima2  25875  i1fadd  25891  itg1addlem4  25895  itg2splitlem  25944  itg2split  25945  ellimc3  26075  limcflflem  26076  limcflf  26077  limcresi  26081  limciun  26090  dvreslem  26105  dvres2lem  26106  dvres  26107  dvaddbr  26134  dvmulbr  26135  dvlip  26189  dvlip2  26191  c1liplem1  26192  dvivthlem1  26204  dvne0  26207  lhop1lem  26209  lhop  26212  dvcnvrelem1  26213  dvcnvrelem2  26214  dvfsumle  26217  dvfsumabs  26219  dvfsumlem2  26223  itgsubstlem  26244  mdegleb  26258  mdeglt  26259  mdegldg  26260  mdegxrcl  26261  mdegcl  26263  ig1peu  26369  reeff1olem  26646  logccv  26865  rlimcnp2  27168  lgamgulmlem2  27231  ppisval  27305  prmdvdsfi  27308  mumul  27382  sqff1o  27383  chtlepsi  27407  chpub  27421  dchrisum0lem2a  27718  pntlem3  27810  nosupno  27904  noetalem1  27942  cutlt  28162  negsproplem2  28259  onsbnd  28511  ex-res  30829  htthlem  31306  chlejb1i  31865  ssmd2  32701  fz2ssnn0  33167  gsumpart  33414  gsumhashmul  33418  elrgspnsubrunlem2  33599  extvfvcl  33957  mplvrpmrhm  33968  esplyind  33996  vietalem  34000  locfinreflem  34261  sibfof  34762  sitgclbn  34765  sitgaddlemb  34770  eulerpartlemgu  34799  ballotlemsima  34938  reprinrn  35037  bnj1311  35444  fnrelpredd  35507  erdsze2lem2  35717  iccllysconn  35763  cvmopnlem  35791  msrf  36055  neiin  36884  neibastop1  36911  neibastop2lem  36912  topmeet  36916  ttciunun  37063  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem11  38323  poimirlem12  38324  poimirlem16  38328  poimirlem19  38331  poimirlem30  38342  cnambfre  38360  itg2gt0cn  38367  sstotbnd2  38466  sstotbnd3  38468  ssbnd  38480  ismtyima  38495  heibor1lem  38501  idresssidinxp  39004  pmodlem2  40662  pmodN  40665  diaintclN  41873  djaclN  41951  dibintclN  41982  dicval  41991  dihoml4c  42191  djhcl  42215  infdesc  43416  isnacs2  43478  isnacs3  43482  diophrw  43531  pellfundre  43649  pellfundge  43650  pellfundlb  43652  pellfundglb  43653  fnwe2lem2  43819  lmhmfgima  43852  hbt  43898  omabs2  44100  nadd2rabord  44153  nadd1rabord  44157  cnvtrcl0  44393  trclrelexplem  44478  relexp0a  44483  isotone2  44816  imo72b2lem1  44936  tcfr  45713  modelaxreplem1  45728  wfac8prim  45752  climinf  46363  islptre  46376  limccog  46377  limcleqr  46399  limsupvaluz2  46493  itgcoscmulx  46724  ismbl3  46741  ismbl4  46748  stoweidlem27  46782  dirkercncflem2  46859  fourierdlem38  46900  fourierdlem51  46912  fourierdlem54  46915  fourierdlem63  46924  fourierdlem68  46929  fourierdlem69  46930  fourierdlem70  46931  fourierdlem74  46935  fourierdlem75  46936  fourierdlem76  46937  fourierdlem80  46941  fourierdlem84  46945  fourierdlem85  46946  fourierdlem88  46949  fourierdlem100  46961  fourierdlem101  46962  fourierdlem104  46965  fourierdlem107  46968  fourierdlem111  46972  fourierdlem112  46973  caragenel2d  47287  hoidmv1lelem3  47348  hspmbllem3  47383  sssmf  47493  smfrec  47544  smfsuplem1  47566