MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sstrd Structured version   Unicode version

Theorem sstrd 3480
Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
Hypotheses
Ref Expression
sstrd.1  |-  ( ph  ->  A  C_  B )
sstrd.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
sstrd  |-  ( ph  ->  A  C_  C )

Proof of Theorem sstrd
StepHypRef Expression
1 sstrd.1 . 2  |-  ( ph  ->  A  C_  B )
2 sstrd.2 . 2  |-  ( ph  ->  B  C_  C )
3 sstr 3478 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  syl5ss  3481  syl6ss  3482  ssdif2d  3610  uniintsn  4296  funss  5619  fssxp  5758  knatar  6263  tfisi  6699  suppfnss  6951  suppssov1  6958  suppssfv  6962  tposss  6982  tfrlem1  7102  omwordri  7281  oewordri  7301  oeeui  7311  oaabs2  7354  omopthlem1  7364  ecinxp  7446  sbthlem1  7688  dffi2  7943  hartogslem1  8057  cantnfcl  8171  cantnflt  8176  cantnfp1lem3  8184  cantnflem3  8195  cnfcom  8204  cnfcom3lem  8207  rankssb  8318  tskwe  8383  dfac12lem2  8572  dfac12lem3  8573  cfflb  8687  cfcof  8702  ssfin2  8748  hsmexlem4  8857  ttukeylem6  8942  ttukeylem7  8943  fpwwe2lem1  9055  fpwwe2lem8  9061  fpwwe2lem11  9064  fpwwe2lem12  9065  canthnumlem  9072  canthwelem  9074  canthwe  9075  canthp1lem2  9077  pwfseqlem5  9087  wunex2  9162  tsktrss  9185  inttsk  9198  uzwo3  11259  supicc  11778  supiccub  11779  supicclub  11780  seqsplit  12243  seqf1olem2a  12248  seqz  12258  swrdval2  12761  trrelssd  13016  rtrclreclem4  13103  sumss  13768  qshash  13863  incexc  13873  incexc2  13874  prodss  13979  rpnnen2lem11  14255  vdwlem1  14885  ramub1lem1  14938  imasaddvallem  15377  imasvscaf  15387  mrerintcl  15445  ismred2  15451  mremre  15452  mrcuni  15469  mressmrcd  15475  submrc  15476  mrissmrid  15489  mreexexlem2d  15493  isacs2  15501  isacs1i  15505  invss  15608  ssctr  15672  funcres2b  15744  isacs3lem  16354  acsfiindd  16365  acsmapd  16366  acsmap2d  16367  tsrdir  16426  subsubm  16546  gsumwspan  16572  subsubg  16782  subgint  16783  cntzidss  16933  symggen  17053  pmtrdifellem1  17059  pmtrdifellem2  17060  pgpssslw  17192  lsmless1x  17222  lsmless2x  17223  lsmless12  17239  subglsm  17249  gsumval3lem2  17466  gsumzaddlem  17480  gsumzadd  17481  gsum2d  17530  dmdprdd  17557  dprdfeq0  17581  dprdspan  17586  dprdres  17587  dprdss  17588  dprdz  17589  subgdmdprd  17593  subgdprd  17594  dprdsn  17595  dprd2dlem1  17600  dprd2da  17601  dmdprdsplit2lem  17604  dprdsplit  17607  pgpfac1lem2  17634  pgpfac1lem3  17636  pgpfac1lem5  17638  subsubrg  17960  lspss  18133  lspun  18136  lsslsp  18164  lmhmlsp  18198  lsmelval2  18234  lsmssspx  18237  lsppratlem2  18297  lsppratlem3  18298  lsppratlem4  18299  lbsextlem2  18308  lbsextlem3  18309  aspss  18482  ocvlsp  19161  cssmre  19178  obselocv  19213  obslbs  19215  toponmre  20031  neiint  20042  neiss  20047  lpss  20080  lpss3  20082  restopnb  20113  restfpw  20117  neitr  20118  restcls  20119  restntr  20120  restlp  20121  ordtbas  20130  pnfnei  20158  mnfnei  20159  iscnp4  20201  cnclsi  20210  isreg2  20315  discmp  20335  cmpcld  20339  uncmp  20340  sscmp  20342  hauscmplem  20343  cmpfi  20345  iunconlem  20364  clscon  20367  2ndcctbss  20392  restnlly  20419  llyrest  20422  nllyrest  20423  llyidm  20425  nllyidm  20426  cldllycmp  20432  dislly  20434  comppfsc  20469  llycmpkgen2  20487  ptbasfi  20518  txnlly  20574  txcmplem1  20578  tx1stc  20587  xkococnlem  20596  qtopval2  20633  basqtop  20648  tgqtop  20649  qtoprest  20654  kqreglem1  20678  kqreglem2  20679  kqnrmlem1  20680  kqnrmlem2  20681  fsubbas  20804  fgabs  20816  fbasrn  20821  trfil2  20824  trfg  20828  isufil2  20845  trufil  20847  ssufl  20855  ufileu  20856  filufint  20857  fmfnfmlem4  20894  fmfnfm  20895  flimss2  20909  flimss1  20910  fclsfnflim  20964  flimfnfcls  20965  fclscmp  20967  cnpfcfi  20977  alexsubALT  20988  clssubg  21045  clsnsg  21046  tsmsres  21080  ustexsym  21152  ustex2sym  21153  ustex3sym  21154  ustund  21158  ustneism  21160  trust  21166  utoptop  21171  restutopopn  21175  utop2nei  21187  utopreg  21189  cfiluweak  21232  neipcfilu  21233  blssps  21361  blss  21362  blcld  21442  blsscls  21444  met1stc  21458  met2ndci  21459  metust  21495  cfilucfil  21496  restmetu  21507  tgqioo  21720  xrsblre  21731  reconnlem2  21747  xrge0gsumle  21753  xrge0tsms  21754  rescncf  21816  cnmpt2pc  21843  cnheibor  21870  cnllycmp  21871  lebnum  21879  phtpycn  21898  cfilfcls  22128  iscmet3lem2  22146  cmetss  22168  cncmet  22174  bcthlem4  22179  bcth3  22183  rrxcph  22235  rrxmetlem  22245  minveclem4a  22256  minveclem4  22258  ivthicc  22281  ovollb  22301  ovollb2lem  22310  ovollb2  22311  nulmbl2  22358  ioorcl2  22392  uniioombllem3  22411  uniioombllem4  22412  uniioombllem5  22413  opnmbllem  22427  volcn  22432  volivth  22433  mbfeqalem  22466  itg10a  22536  mbfi1fseqlem4  22544  ditgcl  22681  ditgswap  22682  ditgsplitlem  22683  limcflf  22704  limcres  22709  dvbss  22724  dvbsss  22725  perfdvf  22726  dvreslem  22732  dvres2lem  22733  dvres3  22736  dvcnp  22741  dvcnp2  22742  dvcn  22743  dvnff  22745  dvn2bss  22752  dvnres  22753  cpnord  22757  dvaddbr  22760  dvmulbr  22761  dvcobr  22768  dvnfre  22774  dvmptres2  22784  dvmptntr  22793  dvcnvlem  22796  dvcnv  22797  dvferm1lem  22804  dvferm2lem  22806  dvlip  22813  dvlipcn  22814  dvlip2  22815  c1liplem1  22816  dvgt0lem1  22822  lhop1lem  22833  lhop  22836  dvcnvrelem1  22837  dvcnvrelem2  22838  dvcnvre  22839  dvfsumle  22841  dvfsumge  22842  dvfsumabs  22843  ftc1lem1  22855  ftc1lem2  22856  ftc1a  22857  ftc1lem4  22859  ftc2ditglem  22865  itgsubstlem  22868  ig1peu  22988  ig1pdvds  22993  taylfvallem1  23168  tayl0  23173  taylply2  23179  taylply  23180  dvtaylp  23181  dvntaylp  23182  dvntaylp0  23183  taylthlem1  23184  ulmdvlem1  23211  ulmdvlem3  23213  psercn  23237  pserdvlem2  23239  abelth  23252  xrlimcnp  23750  lgamucov  23819  wilthlem2  23850  sqff1o  23963  chtublem  23993  pntlemq  24293  pntlemf  24297  tglineintmo  24537  ttgcontlem1  24752  ghsubgolemOLD  25934  shintcli  26808  shub1  26861  mdslmd1lem1  27804  mdexchi  27814  chirredlem1  27869  mdsymlem5  27886  sumdmdii  27894  sumdmdlem2  27898  xrsupssd  28171  xrge0infssd  28173  xrge0tsmsd  28378  smatrcl  28452  locfinreflem  28497  cmpcref  28507  pnfneige0  28587  esum2d  28744  insiga  28789  sssigagen2  28798  dynkin  28819  dya2iocnei  28934  omsmon  28950  carsgclctunlem1  28969  carsggect  28970  omsmeas  28975  bnj906  29520  bnj1020  29553  bnj1137  29583  bnj1408  29624  bnj1452  29640  erdszelem7  29699  erdszelem8  29700  erdsze2lem1  29705  conpcon  29737  cvmliftmolem1  29783  cvmlift2lem1  29804  cvmlift2lem9  29813  cvmlift2lem10  29814  cvmlift3lem6  29826  cvmlift3lem7  29827  ss2mcls  29985  dftrpred3g  30252  nofulllem3  30369  neibastop2lem  30792  fnemeet2  30799  fnejoin1  30800  ontgval  30867  opnmbllem0  31670  ftc1anclem7  31717  ftc1anclem8  31718  ftc1anc  31719  sstotbnd2  31800  heiborlem1  31837  heiborlem8  31844  intidl  31956  lsmsat  32273  lssats  32277  lpssat  32278  lssatle  32280  lssat  32281  lsatcvatlem  32314  paddss12  33083  paddasslem17  33100  pmodlem1  33110  pmod1i  33112  pmodl42N  33115  elpcliN  33157  pclfinN  33164  polcon3N  33181  polcon2N  33183  paddunN  33191  pclfinclN  33214  poml5N  33218  osumcllem1N  33220  osumcllem2N  33221  osumcllem3N  33222  pl42lem2N  33244  pl42lem4N  33246  cdlemn5pre  34467  dihord1  34485  dihord2a  34486  dihord2b  34487  dihord5b  34526  dochss  34632  dochdmj1  34657  djhsumss  34674  djhunssN  34676  dochexmidlem2  34728  lclkrslem1  34804  lclkrslem2  34805  lcfrlem2  34810  elrfi  35235  ismrcd1  35239  istopclsd  35241  mrefg2  35248  aomclem2  35609  aomclem6  35613  hbtlem6  35684  hbt  35685  dfrcl2  35895  relexp0a  35937  trclimalb2  35947  frege81d  35968  imo72b2lem0  36235  imo72b2lem2  36237  imo72b2lem1  36241  imo72b2  36246  uzwo4  37023  ssin0  37026  fimass  37055  supxrre3  37147  uzfissfz  37148  limccog  37262  limclner  37294  cncfmptssg  37309  cncfuni  37326  icccncfext  37327  dvresntr  37350  dvmptresicc  37353  dvbdfbdioolem1  37362  dvdmsscn  37370  dvnxpaek  37376  dvnprodlem2  37381  stoweidlem59  37479  fourierdlem20  37548  fourierdlem42  37570  fourierdlem48  37576  fourierdlem49  37577  fourierdlem52  37580  fourierdlem58  37586  fourierdlem64  37592  fourierdlem73  37601  fourierdlem76  37604  fourierdlem80  37608  fourierdlem84  37612  fourierdlem93  37621  fourierdlem103  37631  fourierdlem104  37632  fourierdlem113  37641  etransclem18  37674  salincl  37721  intsal  37726  fsumlesge0  37743  sge0cl  37747  sge0supre  37755  sge0less  37758  sge0split  37775  caragensspw  37829  omessre  37830  caragendifcl  37834  caratheodorylem1  37846  subsubmgm  38545
  Copyright terms: Public domain W3C validator