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

Theorem sstrd 3410
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 3408 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 671 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386
This theorem is referenced by:  syl5ss  3411  syl6ss  3412  ssdif2d  3540  uniintsn  4242  funss  5579  fssxp  5724  knatar  6234  tfisi  6673  suppfnss  6928  suppssov1  6935  suppssfv  6939  tposss  6961  tfrlem1  7081  omwordri  7260  oewordri  7280  oeeui  7290  oaabs2  7333  omopthlem1  7343  ecinxp  7425  sbthlem1  7669  dffi2  7924  hartogslem1  8044  cantnfcl  8159  cantnflt  8164  cantnfp1lem3  8172  cantnflem3  8183  cnfcom  8192  cnfcom3lem  8195  rankssb  8306  tskwe  8371  dfac12lem2  8561  dfac12lem3  8562  cfflb  8676  cfcof  8691  ssfin2  8737  hsmexlem4  8846  ttukeylem6  8931  ttukeylem7  8932  fpwwe2lem1  9043  fpwwe2lem8  9049  fpwwe2lem11  9052  fpwwe2lem12  9053  canthnumlem  9060  canthwelem  9062  canthwe  9063  canthp1lem2  9065  pwfseqlem5  9075  wunex2  9150  tsktrss  9173  inttsk  9186  uzwo3  11249  supicc  11771  supiccub  11772  supicclub  11773  seqsplit  12240  seqf1olem2a  12245  seqz  12255  swrdval2  12775  trrelssd  13048  rtrclreclem4  13135  sumss  13801  qshash  13896  incexc  13906  incexc2  13907  prodss  14012  rpnnen2lem11  14288  vdwlem1  14942  ramub1lem1  14995  imasaddvallem  15446  imasvscaf  15456  mrerintcl  15514  ismred2  15520  mremre  15521  mrcuni  15538  mressmrcd  15544  submrc  15545  mrissmrid  15558  mreexexlem2d  15562  isacs2  15570  isacs1i  15574  invss  15677  ssctr  15741  funcres2b  15813  isacs3lem  16423  acsfiindd  16434  acsmapd  16435  acsmap2d  16436  tsrdir  16495  subsubm  16615  gsumwspan  16641  subsubg  16851  subgint  16852  cntzidss  17002  symggen  17122  pmtrdifellem1  17128  pmtrdifellem2  17129  pgpssslw  17277  lsmless1x  17307  lsmless2x  17308  lsmless12  17324  subglsm  17334  gsumval3lem2  17551  gsumzaddlem  17565  gsumzadd  17566  gsum2d  17615  dmdprdd  17642  dprdfeq0  17666  dprdspan  17671  dprdres  17672  dprdss  17673  dprdz  17674  subgdmdprd  17678  subgdprd  17679  dprdsn  17680  dprd2dlem1  17685  dprd2da  17686  dmdprdsplit2lem  17689  dprdsplit  17692  pgpfac1lem2  17719  pgpfac1lem3  17721  pgpfac1lem5  17723  subsubrg  18045  lspss  18218  lspun  18221  lsslsp  18249  lmhmlsp  18283  lsmelval2  18319  lsmssspx  18322  lsppratlem2  18382  lsppratlem3  18383  lsppratlem4  18384  lbsextlem2  18393  lbsextlem3  18394  aspss  18567  ocvlsp  19250  cssmre  19267  obselocv  19302  obslbs  19304  toponmre  20120  neiint  20131  neiss  20136  lpss  20169  lpss3  20171  restopnb  20202  restfpw  20206  neitr  20207  restcls  20208  restntr  20209  restlp  20210  ordtbas  20219  pnfnei  20247  mnfnei  20248  iscnp4  20290  cnclsi  20299  isreg2  20404  discmp  20424  cmpcld  20428  uncmp  20429  sscmp  20431  hauscmplem  20432  cmpfi  20434  iunconlem  20453  clscon  20456  2ndcctbss  20481  restnlly  20508  llyrest  20511  nllyrest  20512  llyidm  20514  nllyidm  20515  cldllycmp  20521  dislly  20523  comppfsc  20558  llycmpkgen2  20576  ptbasfi  20607  txnlly  20663  txcmplem1  20667  tx1stc  20676  xkococnlem  20685  qtopval2  20722  basqtop  20737  tgqtop  20738  qtoprest  20743  kqreglem1  20767  kqreglem2  20768  kqnrmlem1  20769  kqnrmlem2  20770  fsubbas  20893  fgabs  20905  fbasrn  20910  trfil2  20913  trfg  20917  isufil2  20934  trufil  20936  ssufl  20944  ufileu  20945  filufint  20946  fmfnfmlem4  20983  fmfnfm  20984  flimss2  20998  flimss1  20999  fclsfnflim  21053  flimfnfcls  21054  fclscmp  21056  cnpfcfi  21066  alexsubALT  21077  clssubg  21134  clsnsg  21135  tsmsres  21169  ustexsym  21241  ustex2sym  21242  ustex3sym  21243  ustund  21247  ustneism  21249  trust  21255  utoptop  21260  restutopopn  21264  utop2nei  21276  utopreg  21278  cfiluweak  21321  neipcfilu  21322  blssps  21450  blss  21451  blcld  21531  blsscls  21533  met1stc  21547  met2ndci  21548  metust  21584  cfilucfil  21585  restmetu  21596  tgqioo  21829  xrsblre  21840  reconnlem2  21856  xrge0gsumle  21862  xrge0tsms  21863  rescncf  21940  cnmpt2pc  21967  cnheibor  21994  cnllycmp  21995  lebnum  22006  phtpycn  22025  cfilfcls  22255  iscmet3lem2  22273  cmetss  22295  cncmet  22301  bcthlem4  22306  bcth3  22310  rrxcph  22362  rrxmetlem  22372  minveclem4a  22383  minveclem4  22385  minveclem4aOLD  22395  minveclem4OLD  22397  ivthicc  22420  ovollb  22443  ovollb2lem  22452  ovollb2  22453  nulmbl2  22501  ioorcl2  22536  uniioombllem3  22555  uniioombllem4  22556  uniioombllem5  22557  opnmbllem  22571  volcn  22576  volivth  22577  mbfeqalem  22610  itg10a  22680  mbfi1fseqlem4  22688  ditgcl  22825  ditgswap  22826  ditgsplitlem  22827  limcflf  22848  limcres  22853  dvbss  22868  dvbsss  22869  perfdvf  22870  dvreslem  22876  dvres2lem  22877  dvres3  22880  dvcnp  22885  dvcnp2  22886  dvcn  22887  dvnff  22889  dvn2bss  22896  dvnres  22897  cpnord  22901  dvaddbr  22904  dvmulbr  22905  dvcobr  22912  dvnfre  22918  dvmptres2  22928  dvmptntr  22937  dvcnvlem  22940  dvcnv  22941  dvferm1lem  22948  dvferm2lem  22950  dvlip  22957  dvlipcn  22958  dvlip2  22959  c1liplem1  22960  dvgt0lem1  22966  lhop1lem  22977  lhop  22980  dvcnvrelem1  22981  dvcnvrelem2  22982  dvcnvre  22983  dvfsumle  22985  dvfsumge  22986  dvfsumabs  22987  ftc1lem1  22999  ftc1lem2  23000  ftc1a  23001  ftc1lem4  23003  ftc2ditglem  23009  itgsubstlem  23012  ig1peu  23134  ig1peuOLD  23135  ig1pdvds  23140  ig1pdvdsOLD  23146  taylfvallem1  23324  tayl0  23329  taylply2  23335  taylply  23336  dvtaylp  23337  dvntaylp  23338  dvntaylp0  23339  taylthlem1  23340  ulmdvlem1  23367  ulmdvlem3  23369  psercn  23393  pserdvlem2  23395  abelth  23408  xrlimcnp  23906  lgamucov  23975  wilthlem2  24006  sqff1o  24121  chtublem  24151  pntlemq  24451  pntlemf  24455  tglineintmo  24699  ttgcontlem1  24927  ghsubgolemOLD  26110  shintcli  26994  shub1  27047  mdslmd1lem1  27990  mdexchi  28000  chirredlem1  28055  mdsymlem5  28072  sumdmdii  28080  sumdmdlem2  28084  xrsupssd  28347  xrge0infssd  28350  xrge0infssdOLD  28351  xrge0tsmsd  28555  smatrcl  28629  locfinreflem  28674  cmpcref  28684  pnfneige0  28764  esum2d  28921  insiga  28966  sssigagen2  28975  dynkin  28996  dya2iocnei  29110  omsmon  29132  omsmonOLD  29136  carsgclctunlem1  29155  carsggect  29156  omsmeas  29161  omsmeasOLD  29162  bnj906  29747  bnj1020  29780  bnj1137  29810  bnj1408  29851  bnj1452  29867  erdszelem7  29926  erdszelem8  29927  erdsze2lem1  29932  conpcon  29964  cvmliftmolem1  30010  cvmlift2lem1  30031  cvmlift2lem9  30040  cvmlift2lem10  30041  cvmlift3lem6  30053  cvmlift3lem7  30054  ss2mcls  30212  dftrpred3g  30480  nofulllem3  30599  neibastop2lem  31022  fnemeet2  31029  fnejoin1  31030  ontgval  31097  opnmbllem0  31978  ftc1anclem7  32025  ftc1anclem8  32026  ftc1anc  32027  sstotbnd2  32108  heiborlem1  32145  heiborlem8  32152  intidl  32264  lsmsat  32576  lssats  32580  lpssat  32581  lssatle  32583  lssat  32584  lsatcvatlem  32617  paddss12  33386  paddasslem17  33403  pmodlem1  33413  pmod1i  33415  pmodl42N  33418  elpcliN  33460  pclfinN  33467  polcon3N  33484  polcon2N  33486  paddunN  33494  pclfinclN  33517  poml5N  33521  osumcllem1N  33523  osumcllem2N  33524  osumcllem3N  33525  pl42lem2N  33547  pl42lem4N  33549  cdlemn5pre  34770  dihord1  34788  dihord2a  34789  dihord2b  34790  dihord5b  34829  dochss  34935  dochdmj1  34960  djhsumss  34977  djhunssN  34979  dochexmidlem2  35031  lclkrslem1  35107  lclkrslem2  35108  lcfrlem2  35113  elrfi  35538  ismrcd1  35542  istopclsd  35544  mrefg2  35551  aomclem2  35915  aomclem6  35919  hbtlem6  35990  hbt  35991  mptrcllem  36222  dfrcl2  36268  relexp0a  36310  trclimalb2  36320  frege81d  36341  imo72b2lem0  36610  imo72b2lem2  36612  imo72b2lem1  36616  imo72b2  36620  uzwo4  37387  ssin0  37390  ixpssmapc  37413  fimass  37453  supxrre3  37579  uzfissfz  37580  ssuzfz  37603  inficc  37677  limccog  37742  limclner  37774  cncfmptssg  37789  cncfuni  37806  icccncfext  37807  dvresntr  37830  dvmptresicc  37833  dvbdfbdioolem1  37842  dvdmsscn  37853  dvnxpaek  37859  dvnprodlem2  37864  stoweidlem59  37977  fourierdlem20  38046  fourierdlem42  38069  fourierdlem42OLD  38070  fourierdlem48  38075  fourierdlem49  38076  fourierdlem52  38079  fourierdlem58  38085  fourierdlem64  38091  fourierdlem73  38100  fourierdlem76  38103  fourierdlem80  38107  fourierdlem84  38111  fourierdlem93  38120  fourierdlem103  38130  fourierdlem104  38131  fourierdlem113  38140  etransclem18  38174  salincl  38241  intsal  38246  fsumlesge0  38278  sge0cl  38282  sge0supre  38290  sge0less  38293  sge0split  38310  sge0seq  38347  caragensspw  38394  omessre  38395  caragendifcl  38399  caratheodorylem1  38411  0ome  38414  omess0  38419  caragencmpl  38420  hoicvr  38433  hoissrrn  38434  hoicvrrex  38441  ovnlecvr  38443  ovnsslelem  38445  ovnssle  38446  ovnsubaddlem1  38455  hoissrrn2  38463  hoidmv1lelem1  38476  hoidmvlelem1  38480  hoidmvlelem2  38481  hoidmvlelem4  38483  ovnlecvr2  38495  voncmpl  38506  hspmbl  38514  opnvonmbllem1  38517  ovolval5lem2  38538  ovolval5lem3  38539  pthdlem1  39844  subsubmgm  40122
  Copyright terms: Public domain W3C validator