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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  difss2  4133  rintn0  5112  eqbrrdva  5868  ssxpb  6171  resssxp  6267  relfld  6272  funssxp  6744  dff2  7098  dff3  7099  fliftf  7309  1stcof  8002  2ndcof  8003  frxp2  8127  frxp3  8134  frrlem13  8280  nnunifi  9291  elfiun  9422  marypha1lem  9425  marypha1  9426  ordtypelem7  9516  tcmin  9733  unwf  9802  rankfu  9869  tcrank  9876  aceq3lem  10112  dfac12lem2  10136  ackbij1lem9  10220  ackbij1lem10  10221  ackbij1lem16  10227  fin23lem26  10317  fin23lem27  10320  fin1a2lem6  10397  itunitc  10413  axdc3lem2  10443  ttukeylem5  10505  fpwwe2lem12  10634  canthwelem  10642  pwfseqlem4  10654  wunex2  10730  wunex3  10733  inar1  10767  inatsk  10770  gruina  10810  suprfinzcl  12673  suprzub  12920  uzsupss  12921  uzwo3  12924  rpnnen1lem4  12961  rpnnen1lem5  12962  supxrre  13303  infxrre  13312  ioodisj  13456  supicclub2  13478  fzssnn  13542  fzossnn0  13660  elfzom1elp1fzo  13696  injresinjlem  13749  uzindi  13944  ssnn0fi  13947  seqcoll  14422  seqcoll2  14423  reltrclfv  14961  relexpdmg  14986  relexpdm  14987  relexprng  14990  relexprn  14991  relexpfld  14993  relexpaddg  14997  limsupval2  15421  limsupgre  15422  limsupbnd2  15424  rlimuni  15491  rlimcld2  15519  rlimno1  15597  isercolllem2  15609  isercoll  15611  summolem2a  15658  summolem2  15659  fsumsers  15671  fsumcvg3  15672  prodmolem2a  15875  prodmolem2  15876  zprod  15878  lcmfnnval  16558  lcmfnncl  16563  4sqlem11  16885  vdwlem8  16918  vdwlem11  16921  ramub2  16944  0ram  16950  0ram2  16951  0ramcl  16953  ramub1lem2  16957  prmgaplem3  16983  prmgaplem4  16984  isohom  17720  funcres2c  17849  resscntz  19192  cntzidss  19199  cntzmhm2  19201  pgpssslw  19477  cntzspan  19707  gsumval3  19770  gsum2d  19835  dprdspan  19892  dprdres  19893  subdrgint  20412  sdrgint  20413  primefld  20414  lssintcl  20568  lbsextlem2  20765  lbsextlem3  20766  lbsextlem4  20767  islinds3  21381  fctop  22499  cctop  22501  neitr  22676  ordtbas2  22687  ordtopn1  22690  ordtopn2  22691  lmss  22794  clsconn  22926  2ndcdisj  22952  2ndcomap  22954  ptbasfi  23077  txcmplem2  23138  hausdiag  23141  txkgen  23148  basqtop  23207  alexsubb  23542  alexsubALTlem4  23546  tsmsres  23640  tsmsxplem1  23649  tsmsxp  23651  ustrel  23708  utop3cls  23748  prdsmet  23868  metustrel  24053  icccmplem2  24331  xrge0tsms  24342  cnmptre  24435  icchmeo  24449  bndth  24466  lebnumlem2  24470  cfilresi  24804  causs  24807  bcthlem5  24837  evthicc  24968  ovolficcss  24978  ovolmge0  24986  ovolgelb  24989  ovollb2lem  24997  ovollb2  24998  ovolunlem1a  25005  ovolunlem1  25006  ovoliunlem1  25011  ovoliunlem2  25012  ovoliun  25014  ovolscalem1  25022  ovolicc1  25025  ovolicc2lem4  25029  ovolicc2  25031  voliunlem2  25060  voliunlem3  25061  ioombl1lem2  25068  ioombl1lem4  25070  uniioovol  25088  uniiccvol  25089  uniioombllem1  25090  uniioombllem2  25092  uniioombllem3  25094  uniioombllem4  25095  uniioombllem6  25097  dyadmbllem  25108  dyadmbl  25109  volcn  25115  vitalilem4  25120  vitalilem5  25121  cnmbf  25168  i1fmul  25205  itg1addlem4  25208  itg1addlem4OLD  25209  itg2seq  25252  dvbssntr  25409  dvreslem  25418  dvcjbr  25458  dvferm1  25494  dvferm2  25496  cmvth  25500  dvlip  25502  lhop1lem  25522  lhop2  25524  lhop  25525  dvcnvrelem2  25527  dvcnvre  25528  dvfsumle  25530  dvfsumge  25531  dvfsumabs  25532  dvfsumlem2  25536  ftc1a  25546  ftc1lem3  25547  ftc1lem6  25550  itgsubstlem  25557  itgpowd  25559  mdegleb  25574  mdeglt  25575  mdegldg  25576  mdegxrcl  25577  mdegcl  25579  deg1mul3le  25626  ig1pdvds  25686  plyeq0lem  25716  aannenlem2  25834  aalioulem3  25839  taylf  25865  taylthlem2  25878  pserulm  25926  psercn2  25927  psercn  25930  reeff1olem  25950  efcvx  25953  loglesqrt  26256  rlimcnp  26460  xrlimcnp  26463  jensen  26483  wilthlem2  26563  vmadivsumb  26976  pntrsumo1  27058  pntlem3  27102  perpln2  27952  axcontlem10  28221  usgrexmplef  28506  nmoxr  30007  nmooge0  30008  nmoolb  30012  nmoubi  30013  ubthlem1  30111  shmodi  30631  nmopxr  31107  nmfnxr  31120  nmoplb  31148  nmopub  31149  nmfnlb  31165  nmfnleub  31166  nmopun  31255  branmfn  31346  mdslj1i  31560  hatomistici  31603  xppreima2  31864  fsuppcurry1  31938  fsuppcurry2  31939  fpwrelmap  31946  infxrge0gelb  31967  prmdvdsbc  32010  gsumpart  32195  xrge0tsmsd  32197  pmtrcnel2  32239  cyc3genpm  32299  1fldgenq  32401  ssmxidllem  32578  zarcmplem  32850  metideq  32862  metider  32863  pstmfval  32865  esumgect  33077  esum2d  33080  sigaclci  33119  insiga  33124  omssubadd  33288  eulerpartlemgs2  33368  ballotlemsima  33503  signsply0  33551  iblidicc  33593  fsum2dsub  33608  reprsuc  33616  reprgt  33622  bnj1145  33993  bnj1137  33995  bnj1136  33997  resconn  34226  cvmliftlem8  34272  cvmlift3lem6  34304  mclsssvlem  34542  mclsind  34550  mclsppslem  34563  gg-icchmeo  35159  gg-psercn2  35167  gg-cmvth  35170  gg-dvfsumle  35171  gg-dvfsumlem2  35172  ivthALT  35209  neibastop1  35233  topjoin  35239  bj-imdirco  36060  ptrecube  36477  poimirlem6  36483  poimirlem15  36492  heicant  36512  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2gt0cn  36532  ftc1cnnc  36549  ftc1anclem3  36552  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  areacirclem2  36566  areacirclem3  36567  areacirclem4  36568  totbndbnd  36646  prdsbnd  36650  heiborlem1  36668  rrnequiv  36692  reheibor  36696  iccbnd  36697  pmapssbaN  38620  2polssN  38775  paddunN  38787  poldmj1N  38788  ispsubcl2N  38807  psubclinN  38808  paddatclN  38809  poml4N  38813  diaglbN  39915  diaintclN  39918  dibglbN  40026  dibintclN  40027  dicssdvh  40046  dihvalrel  40139  dochexmidlem4  40323  infdesc  41382  rmxyelqirrOLD  41635  ttac  41761  hbtlem6  41857  hbt  41858  cnvssb  42323  cnvrcl0  42362  cnvtrrel  42407  relexpaddss  42455  cotrcltrcl  42462  cotrclrcl  42479  frege96d  42486  frege97d  42489  frege109d  42494  frege131d  42501  rfovcnvf1od  42741  isotone2  42786  gneispace  42871  k0004ss1  42888  grumnudlem  43030  uzfissfz  44023  suplesup  44036  ssrexr  44129  limciccioolb  44324  limcicciooub  44340  limcleqr  44347  cnrefiisplem  44532  cncfiooicclem1  44596  ibliccsinexp  44654  iblioosinexp  44656  itgcoscmulx  44672  itgsincmulx  44677  itgsubsticclem  44678  itgiccshift  44683  itgperiod  44684  itgsbtaddcnst  44685  stoweidlem34  44737  stoweidlem59  44762  dirkeritg  44805  dirkercncflem2  44807  fourierdlem20  44830  fourierdlem31  44841  fourierdlem39  44849  fourierdlem42  44852  fourierdlem46  44855  fourierdlem52  44861  fourierdlem53  44862  fourierdlem60  44869  fourierdlem61  44870  fourierdlem62  44871  fourierdlem68  44877  fourierdlem76  44885  fourierdlem85  44894  fourierdlem88  44897  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem93  44902  fourierdlem94  44903  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fouriersw  44934  etransclem46  44983  etransclem48  44985  sge0less  45095  sge0resplit  45109  sge0isum  45130  pimdecfgtioo  45420  pimincfltioo  45421  iccpartipre  46076  bgoldbtbndlem2  46461  setrec1lem4  47689  setrec2fun  47691