Theorem sstrdi 3943

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

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

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 3916

This theorem is used by:  difss2  4085  ssinss1  4191  rintn0  5069  eqbrrdva  5849  ssxpb  6167  relcnvtrg  6263  resssxp  6267  relfld  6272  funssxp  6731  dff2  7092  dff3  7093  fliftf  7316  1stcof  8016  2ndcof  8017  frxp2  8142  frxp3  8149  frrlem13  8297  nnunifi  9261  elfiun  9400  marypha1lem  9403  marypha1  9404  ordtypelem7  9496  tcmin  9718  unwf  9792  rankfu  9859  tcrank  9866  aceq3lem  10123  dfac12lem2  10147  ackbij1lem9  10229  ackbij1lem10  10230  ackbij1lem16  10236  fin23lem26  10327  fin23lem27  10330  fin1a2lem6  10407  itunitc  10423  axdc3lem2  10453  ttukeylem5  10515  fpwwe2lem12  10651  canthwelem  10659  pwfseqlem4  10671  wunex2  10747  wunex3  10750  inar1  10784  inatsk  10787  gruina  10827  suprfinzcl  12735  suprzub  12988  uzsupss  12989  uzwo3  12992  rpnnen1lem4  13030  rpnnen1lem5  13031  supxrre  13379  infxrre  13389  ioodisj  13535  supicclub2  13557  fzssnn  13623  fzossnn0  13746  elfzom1elp1fzo  13788  injresinjlem  13846  uzindi  14046  ssnn0fi  14049  seqcoll  14529  seqcoll2  14530  reltrclfv  15090  relexpdmg  15115  relexpdm  15116  relexprng  15119  relexprn  15120  relexpfld  15122  relexpaddg  15126  limsupval2  15567  limsupgre  15568  limsupbnd2  15570  rlimuni  15637  rlimcld2  15665  rlimno1  15741  isercolllem2  15753  isercoll  15755  summolem2a  15801  summolem2  15802  fsumsers  15814  fsumcvg3  15815  prodmolem2a  16021  prodmolem2  16022  zprod  16024  lcmfnnval  16714  lcmfnncl  16719  prmdvdsbc  16817  4sqlem11  17047  vdwlem8  17080  vdwlem11  17083  ramub2  17106  0ram  17112  0ram2  17113  0ramcl  17115  ramub1lem2  17119  prmgaplem3  17145  prmgaplem4  17146  isohom  17865  funcres2c  17992  resscntz  19460  cntzidss  19467  cntzmhm2  19469  pgpssslw  19741  cntzspan  19971  gsumval3  20034  gsum2d  20099  dprdspan  20156  dprdres  20157  subdrgint  20969  sdrgint  20970  primefld  20971  lssintcl  21148  lbsextlem2  21346  lbsextlem3  21347  lbsextlem4  21348  ssdifidllem  21547  islinds3  22047  fctop  23229  cctop  23231  neitr  23405  ordtbas2  23416  ordtopn1  23419  ordtopn2  23420  lmss  23523  clsconn  23655  2ndcdisj  23682  2ndcomap  23684  ptbasfi  23807  txcmplem2  23868  hausdiag  23871  txkgen  23878  basqtop  23937  alexsubb  24272  alexsubALTlem4  24276  tsmsres  24370  tsmsxplem1  24379  tsmsxp  24381  ustrel  24438  utop3cls  24477  prdsmet  24596  metustrel  24778  icccmplem2  25050  xrge0tsms  25061  cnmptre  25155  icchmeo  25169  bndth  25186  lebnumlem2  25190  cfilresi  25523  causs  25526  bcthlem5  25556  evthicc  25687  ovolficcss  25697  ovolmge0  25705  ovolgelb  25708  ovollb2lem  25716  ovollb2  25717  ovolunlem1a  25724  ovolunlem1  25725  ovoliunlem1  25730  ovoliunlem2  25731  ovoliun  25733  ovolscalem1  25741  ovolicc1  25744  ovolicc2lem4  25748  ovolicc2  25750  voliunlem2  25779  voliunlem3  25780  ioombl1lem2  25787  ioombl1lem4  25789  uniioovol  25807  uniiccvol  25808  uniioombllem1  25809  uniioombllem2  25811  uniioombllem3  25813  uniioombllem4  25814  uniioombllem6  25816  dyadmbllem  25827  dyadmbl  25828  volcn  25834  vitalilem4  25839  vitalilem5  25840  cnmbf  25887  i1fmul  25924  itg1addlem4  25927  itg2seq  25970  dvbssntr  26127  dvreslem  26136  dvcjbr  26176  dvferm1  26212  dvferm2  26214  cmvth  26218  dvlip  26220  lhop1lem  26240  lhop2  26242  lhop  26243  dvcnvrelem2  26245  dvcnvre  26246  dvfsumle  26248  dvfsumge  26249  dvfsumabs  26250  dvfsumlem2  26254  ftc1a  26264  ftc1lem3  26265  ftc1lem6  26268  itgsubstlem  26275  itgpowd  26277  mdegleb  26289  mdeglt  26290  mdegldg  26291  mdegxrcl  26292  mdegcl  26294  deg1mul3le  26342  ig1pdvds  26405  plyeq0lem  26436  aannenlem2  26565  aalioulem3  26570  taylf  26597  taylthlem2  26610  pserulm  26658  psercn2  26659  psercn  26662  reeff1olem  26682  efcvx  26685  loglesqrt  26998  rlimcnp  27202  xrlimcnp  27205  jensen  27225  wilthlem2  27305  vmadivsumb  27719  pntrsumo1  27801  pntlem3  27845  noseqrdgfn  28571  bdaypw2n0bndlem  28728  perpln2  29065  axcontlem10  29430  usgrexmplef  29719  dfpth2  30193  nmoxr  31247  nmooge0  31248  nmoolb  31252  nmoubi  31253  ubthlem1  31351  shmodi  31871  nmopxr  32347  nmfnxr  32360  nmoplb  32388  nmopub  32389  nmfnlb  32405  nmfnleub  32406  nmopun  32495  branmfn  32586  mdslj1i  32800  hatomistici  32843  xppreima2  33124  fsuppcurry1  33195  fsuppcurry2  33196  fpwrelmap  33204  infxrge0gelb  33237  gsumpart  33503  xrge0tsmsd  33513  pmtrcnel2  33530  cyc3genpm  33592  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  1fldgenq  33763  ssmxidllem  33876  mplmulmvr  34049  zarcmplem  34391  metideq  34403  metider  34404  pstmfval  34406  esumgect  34600  esum2d  34603  sigaclci  34642  insiga  34648  omssubadd  34811  eulerpartlemgs2  34891  ballotlemsima  35027  signsply0  35059  iblidicc  35100  fsum2dsub  35115  reprsuc  35123  reprgt  35129  bnj1145  35502  bnj1137  35504  bnj1136  35506  resconn  35825  cvmliftlem8  35871  cvmlift3lem6  35903  mclsssvlem  36141  mclsind  36149  mclsppslem  36162  ivthALT  36954  neibastop1  36978  topjoin  36984  dfttc2g  37125  bj-imdirco  37942  ptrecube  38369  poimirlem6  38375  poimirlem15  38384  heicant  38404  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  itg2gt0cn  38424  ftc1cnnc  38441  ftc1anclem3  38444  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  areacirclem2  38458  areacirclem3  38459  areacirclem4  38460  totbndbnd  38539  prdsbnd  38543  heiborlem1  38561  rrnequiv  38585  reheibor  38589  iccbnd  38590  pmapssbaN  40633  2polssN  40788  paddunN  40800  poldmj1N  40801  ispsubcl2N  40820  psubclinN  40821  paddatclN  40822  poml4N  40826  diaglbN  41928  diaintclN  41931  dibglbN  42039  dibintclN  42040  dicssdvh  42059  dihvalrel  42152  dochexmidlem4  42336  infdesc  43489  ttac  43877  hbtlem6  43970  hbt  43971  cnvssb  44426  cnvrcl0  44465  cnvtrrel  44510  relexpaddss  44558  cotrcltrcl  44565  cotrclrcl  44582  frege96d  44589  frege97d  44592  frege109d  44597  frege131d  44604  rfovcnvf1od  44844  isotone2  44889  gneispace  44974  k0004ss1  44991  grumnudlem  45109  uzfissfz  46156  suplesup  46169  ssrexr  46260  limciccioolb  46451  limcicciooub  46465  limcleqr  46472  cnrefiisplem  46657  cncfiooicclem1  46721  ibliccsinexp  46779  iblioosinexp  46781  itgcoscmulx  46797  itgsincmulx  46802  itgsubsticclem  46803  itgiccshift  46808  itgperiod  46809  itgsbtaddcnst  46810  stoweidlem34  46862  stoweidlem59  46887  dirkeritg  46930  dirkercncflem2  46932  fourierdlem20  46955  fourierdlem31  46966  fourierdlem39  46974  fourierdlem42  46977  fourierdlem46  46980  fourierdlem52  46986  fourierdlem53  46987  fourierdlem60  46994  fourierdlem61  46995  fourierdlem62  46996  fourierdlem68  47002  fourierdlem76  47010  fourierdlem85  47019  fourierdlem88  47022  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem93  47027  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fouriersw  47059  etransclem46  47108  etransclem48  47110  sge0less  47220  sge0resplit  47234  sge0isum  47255  hoicvr  47376  pimdecfgtioo  47545  pimincfltioo  47546  tmachlem-fssscan  47778  iccpartipre  48321  bgoldbtbndlem2  48722  setrec1lem4  50616  setrec2fun  50618