Theorem sstrdi 3979

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

Syntax hints:   → wi 4   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  difss2  4110  rintn0  5030  eqbrrdva  5740  ssxpb  6031  relfld  6126  funssxp  6535  dff2  6865  dff3  6866  fliftf  7068  1stcof  7719  2ndcof  7720  nnunifi  8769  elfiun  8894  marypha1lem  8897  marypha1  8898  ordtypelem7  8988  tcmin  9183  unwf  9239  rankfu  9306  tcrank  9313  aceq3lem  9546  dfac12lem2  9570  ackbij1lem9  9650  ackbij1lem10  9651  ackbij1lem16  9657  fin23lem26  9747  fin23lem27  9750  fin1a2lem6  9827  itunitc  9843  axdc3lem2  9873  ttukeylem5  9935  fpwwe2lem13  10064  canthwelem  10072  pwfseqlem4  10084  wunex2  10160  wunex3  10163  inar1  10197  inatsk  10200  gruina  10240  suprfinzcl  12098  suprzub  12340  uzsupss  12341  uzwo3  12344  rpnnen1lem4  12380  rpnnen1lem5  12381  supxrre  12721  infxrre  12730  ioodisj  12869  supicclub2  12890  fzssnn  12952  fzossnn0  13069  elfzom1elp1fzo  13105  injresinjlem  13158  uzindi  13351  ssnn0fi  13354  seqcoll  13823  seqcoll2  13824  reltrclfv  14377  relexpdmg  14401  relexpdm  14402  relexprng  14405  relexprn  14406  relexpfld  14408  relexpaddg  14412  limsupval2  14837  limsupgre  14838  limsupbnd2  14840  rlimuni  14907  rlimcld2  14935  rlimno1  15010  isercolllem2  15022  isercoll  15024  summolem2a  15072  summolem2  15073  fsumsers  15085  fsumcvg3  15086  prodmolem2a  15288  prodmolem2  15289  zprod  15291  lcmfnnval  15968  lcmfnncl  15973  4sqlem11  16291  vdwlem8  16324  vdwlem11  16327  ramub2  16350  0ram  16356  0ram2  16357  0ramcl  16359  ramub1lem2  16363  prmgaplem3  16389  prmgaplem4  16390  isohom  17046  funcres2c  17171  resscntz  18462  cntzidss  18468  cntzmhm2  18470  pgpssslw  18739  cntzspan  18964  gsumval3  19027  gsum2d  19092  dprdspan  19149  dprdres  19150  subdrgint  19582  sdrgint  19583  primefld  19584  lssintcl  19736  lbsextlem2  19931  lbsextlem3  19932  lbsextlem4  19933  islinds3  20978  fctop  21612  cctop  21614  neitr  21788  ordtbas2  21799  ordtopn1  21802  ordtopn2  21803  lmss  21906  clsconn  22038  2ndcdisj  22064  2ndcomap  22066  ptbasfi  22189  txcmplem2  22250  hausdiag  22253  txkgen  22260  basqtop  22319  alexsubb  22654  alexsubALTlem4  22658  tsmsres  22752  tsmsxplem1  22761  tsmsxp  22763  ustrel  22820  utop3cls  22860  prdsmet  22980  metustrel  23162  icccmplem2  23431  xrge0tsms  23442  cnmptre  23531  icchmeo  23545  bndth  23562  lebnumlem2  23566  cfilresi  23898  causs  23901  bcthlem5  23931  evthicc  24060  ovolficcss  24070  ovolmge0  24078  ovolgelb  24081  ovollb2lem  24089  ovollb2  24090  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliunlem2  24104  ovoliun  24106  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem4  24121  ovolicc2  24123  voliunlem2  24152  voliunlem3  24153  ioombl1lem2  24160  ioombl1lem4  24162  uniioovol  24180  uniiccvol  24181  uniioombllem1  24182  uniioombllem2  24184  uniioombllem3  24186  uniioombllem4  24187  uniioombllem6  24189  dyadmbllem  24200  dyadmbl  24201  volcn  24207  vitalilem4  24212  vitalilem5  24213  cnmbf  24260  i1fmul  24297  itg1addlem4  24300  itg2seq  24343  dvbssntr  24498  dvreslem  24507  dvcjbr  24546  dvferm1  24582  dvferm2  24584  cmvth  24588  dvlip  24590  lhop1lem  24610  lhop2  24612  lhop  24613  dvcnvrelem2  24615  dvcnvre  24616  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem2  24624  ftc1a  24634  ftc1lem3  24635  ftc1lem6  24638  itgsubstlem  24645  mdegleb  24658  mdeglt  24659  mdegldg  24660  mdegxrcl  24661  mdegcl  24663  deg1mul3le  24710  ig1pdvds  24770  plyeq0lem  24800  aannenlem2  24918  aalioulem3  24923  taylf  24949  taylthlem2  24962  pserulm  25010  psercn2  25011  psercn  25014  reeff1olem  25034  efcvx  25037  loglesqrt  25339  rlimcnp  25543  xrlimcnp  25546  jensen  25566  wilthlem2  25646  vmadivsumb  26059  pntrsumo1  26141  pntlem3  26185  perpln2  26497  axcontlem10  26759  usgrexmplef  27041  nmoxr  28543  nmooge0  28544  nmoolb  28548  nmoubi  28549  ubthlem1  28647  shmodi  29167  nmopxr  29643  nmfnxr  29656  nmoplb  29684  nmopub  29685  nmfnlb  29701  nmfnleub  29702  nmopun  29791  branmfn  29882  mdslj1i  30096  hatomistici  30139  xppreima2  30395  fsuppcurry1  30461  fsuppcurry2  30462  fpwrelmap  30469  infxrge0gelb  30490  prmdvdsbc  30532  xrge0tsmsd  30692  pmtrcnel2  30734  cyc3genpm  30794  ssmxidllem  30978  metideq  31133  metider  31134  pstmfval  31136  esumgect  31349  esum2d  31352  sigaclci  31391  insiga  31396  omssubadd  31558  eulerpartlemgs2  31638  ballotlemsima  31773  signsply0  31821  iblidicc  31863  fsum2dsub  31878  reprsuc  31886  reprgt  31892  bnj1145  32265  bnj1137  32267  bnj1136  32269  resconn  32493  cvmliftlem8  32539  cvmlift3lem6  32571  mclsssvlem  32809  mclsind  32817  mclsppslem  32830  frrlem13  33135  nosupbday  33205  ivthALT  33683  neibastop1  33707  topjoin  33713  ptrecube  34907  poimirlem6  34913  poimirlem15  34922  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2gt0cn  34962  ftc1cnnc  34981  ftc1anclem3  34984  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  areacirclem2  34998  areacirclem3  34999  areacirclem4  35000  totbndbnd  35082  prdsbnd  35086  heiborlem1  35104  rrnequiv  35128  reheibor  35132  iccbnd  35133  pmapssbaN  36911  2polssN  37066  paddunN  37078  poldmj1N  37079  ispsubcl2N  37098  psubclinN  37099  paddatclN  37100  poml4N  37104  diaglbN  38206  diaintclN  38209  dibglbN  38317  dibintclN  38318  dicssdvh  38337  dihvalrel  38430  dochexmidlem4  38614  rmxyelqirr  39556  ttac  39682  hbtlem6  39778  hbt  39779  itgpowd  39870  cnvssb  39995  cnvrcl0  40034  cnvtrrel  40064  relexpaddss  40112  cotrcltrcl  40119  cotrclrcl  40136  frege96d  40143  frege97d  40146  frege109d  40151  frege131d  40158  rp-imass  40166  rfovcnvf1od  40399  isotone2  40448  gneispace  40533  k0004ss1  40550  grumnudlem  40670  uzfissfz  41643  suplesup  41656  ssrexr  41755  limciccioolb  41951  limcicciooub  41967  limcleqr  41974  cnrefiisplem  42159  cncfiooicclem1  42225  ibliccsinexp  42285  iblioosinexp  42287  itgcoscmulx  42303  itgsincmulx  42308  itgsubsticclem  42309  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  stoweidlem34  42368  stoweidlem59  42393  dirkeritg  42436  dirkercncflem2  42438  fourierdlem20  42461  fourierdlem31  42472  fourierdlem39  42480  fourierdlem42  42483  fourierdlem46  42486  fourierdlem52  42492  fourierdlem53  42493  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem68  42508  fourierdlem76  42516  fourierdlem85  42525  fourierdlem88  42528  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem93  42533  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fouriersw  42565  etransclem46  42614  etransclem48  42616  sge0less  42723  sge0resplit  42737  sge0isum  42758  pimdecfgtioo  43044  pimincfltioo  43045  iccpartipre  43630  bgoldbtbndlem2  44020  setrec1lem4  44842  setrec2fun  44844