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

Theorem sstrd 3427
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 3425 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  syl5ss  3428  syl6ss  3429  ssdif2d  3557  uniintsn  4237  funss  5514  fssxp  5651  knatar  6154  suppssfvOLD  6430  suppssov1OLD  6431  tfisi  6592  suppfnss  6843  suppssov1  6850  suppssfv  6854  tposss  6874  tfrlem1  6963  omwordri  7139  oewordri  7159  oeeui  7169  oaabs2  7212  omopthlem1  7222  ecinxp  7304  sbthlem1  7546  dffi2  7798  hartogslem1  7882  cantnfcl  7999  cantnflt  8004  cantnfp1lem3  8012  cantnflem3  8023  cantnfclOLD  8029  cantnfltOLD  8034  cantnfp1lem3OLD  8038  cantnflem3OLD  8045  cnfcom  8057  cnfcom3lem  8060  cnfcomOLD  8065  cnfcom3lemOLD  8068  rankssb  8179  tskwe  8244  dfac12lem2  8437  dfac12lem3  8438  cfflb  8552  cfcof  8567  ssfin2  8613  hsmexlem4  8722  ttukeylem6  8807  ttukeylem7  8808  fpwwe2lem1  8920  fpwwe2lem8  8926  fpwwe2lem11  8929  fpwwe2lem12  8930  canthnumlem  8937  canthwelem  8939  canthwe  8940  canthp1lem2  8942  pwfseqlem5  8952  wunex2  9027  tsktrss  9050  inttsk  9063  uzwo3  11096  supicc  11589  supiccub  11590  supicclub  11591  seqsplit  12043  seqf1olem2a  12048  seqz  12058  swrdval2  12556  trrelssd  12811  rtrclreclem4  12896  sumss  13548  qshash  13641  incexc  13651  incexc2  13652  prodss  13756  rpnnen2lem11  13960  vdwlem1  14501  ramub1lem1  14546  imasaddvallem  14936  imasvscaf  14946  mrerintcl  15004  ismred2  15010  mremre  15011  mrcuni  15028  mressmrcd  15034  submrc  15035  mrissmrid  15048  mreexexlem2d  15052  isacs2  15060  isacs1i  15064  invss  15167  ssctr  15231  funcres2b  15303  isacs3lem  15913  acsfiindd  15924  acsmapd  15925  acsmap2d  15926  tsrdir  15985  subsubm  16105  gsumwspan  16131  subsubg  16341  subgint  16342  cntzidss  16492  symggen  16612  pmtrdifellem1  16618  pmtrdifellem2  16619  pgpssslw  16751  lsmless1x  16781  lsmless2x  16782  lsmless12  16798  subglsm  16808  gsumval3OLD  17025  gsumval3lem2  17027  gsumzaddlem  17051  gsumzadd  17052  gsumzaddOLD  17054  gsum2d  17113  gsum2dOLD  17114  dmdprdd  17143  dprdfeq0  17175  dprdfeq0OLD  17182  dprdspan  17187  dprdres  17188  dprdss  17189  dprdz  17190  subgdmdprd  17194  subgdprd  17195  dprdsn  17196  dprd2dlem1  17203  dprd2da  17204  dmdprdsplit2lem  17207  dprdsplit  17210  pgpfac1lem2  17239  pgpfac1lem3  17241  pgpfac1lem5  17243  subsubrg  17568  lspss  17743  lspun  17746  lsslsp  17774  lmhmlsp  17808  lsmelval2  17844  lsmssspx  17847  lsppratlem2  17907  lsppratlem3  17908  lsppratlem4  17909  lbsextlem2  17918  lbsextlem3  17919  aspss  18094  ocvlsp  18798  cssmre  18815  obselocv  18850  obslbs  18852  toponmre  19680  neiint  19691  neiss  19696  lpss  19729  lpss3  19731  restopnb  19762  restfpw  19766  neitr  19767  restcls  19768  restntr  19769  restlp  19770  ordtbas  19779  pnfnei  19807  mnfnei  19808  iscnp4  19850  cnclsi  19859  isreg2  19964  discmp  19984  cmpcld  19988  uncmp  19989  sscmp  19991  hauscmplem  19992  cmpfi  19994  iunconlem  20013  clscon  20016  2ndcctbss  20041  restnlly  20068  llyrest  20071  nllyrest  20072  llyidm  20074  nllyidm  20075  cldllycmp  20081  dislly  20083  comppfsc  20118  llycmpkgen2  20136  ptbasfi  20167  txnlly  20223  txcmplem1  20227  tx1stc  20236  xkococnlem  20245  qtopval2  20282  basqtop  20297  tgqtop  20298  qtoprest  20303  kqreglem1  20327  kqreglem2  20328  kqnrmlem1  20329  kqnrmlem2  20330  fsubbas  20453  fgabs  20465  fbasrn  20470  trfil2  20473  trfg  20477  isufil2  20494  trufil  20496  ssufl  20504  ufileu  20505  filufint  20506  fmfnfmlem4  20543  fmfnfm  20544  flimss2  20558  flimss1  20559  fclsfnflim  20613  flimfnfcls  20614  fclscmp  20616  cnpfcfi  20626  alexsubALT  20636  clssubg  20692  clsnsg  20693  tsmsres  20731  ustexsym  20803  ustex2sym  20804  ustex3sym  20805  ustund  20809  ustneism  20811  trust  20817  utoptop  20822  restutopopn  20826  utop2nei  20838  utopreg  20840  cfiluweak  20883  neipcfilu  20884  blssps  21012  blss  21013  blcld  21093  blsscls  21095  met1stc  21109  met2ndci  21110  metustOLD  21155  metust  21156  cfilucfilOLD  21157  cfilucfil  21158  restmetu  21175  tgqioo  21390  xrsblre  21401  reconnlem2  21417  xrge0gsumle  21423  xrge0tsms  21424  rescncf  21486  cnmpt2pc  21513  cnheibor  21540  cnllycmp  21541  lebnum  21549  phtpycn  21568  cfilfcls  21798  iscmet3lem2  21816  cmetss  21838  cncmet  21846  bcthlem4  21851  bcth3  21855  rrxcph  21909  rrxmetlem  21919  minveclem4a  21930  minveclem4  21932  ivthicc  21955  ovollb  21975  ovollb2lem  21984  ovollb2  21985  nulmbl2  22032  ioorcl2  22066  uniioombllem3  22079  uniioombllem4  22080  uniioombllem5  22081  opnmbllem  22095  volcn  22100  volivth  22101  mbfeqalem  22134  itg10a  22202  mbfi1fseqlem4  22210  ditgcl  22347  ditgswap  22348  ditgsplitlem  22349  limcflf  22370  limcres  22375  dvbss  22390  dvbsss  22391  perfdvf  22392  dvreslem  22398  dvres2lem  22399  dvres3  22402  dvcnp  22407  dvcnp2  22408  dvcn  22409  dvnff  22411  dvn2bss  22418  dvnres  22419  cpnord  22423  dvaddbr  22426  dvmulbr  22427  dvcobr  22434  dvnfre  22440  dvmptres2  22450  dvmptntr  22459  dvcnvlem  22462  dvcnv  22463  dvferm1lem  22470  dvferm2lem  22472  dvlip  22479  dvlipcn  22480  dvlip2  22481  c1liplem1  22482  dvgt0lem1  22488  lhop1lem  22499  lhop  22502  dvcnvrelem1  22503  dvcnvrelem2  22504  dvcnvre  22505  dvfsumle  22507  dvfsumge  22508  dvfsumabs  22509  ftc1lem1  22521  ftc1lem2  22522  ftc1a  22523  ftc1lem4  22525  ftc2ditglem  22531  itgsubstlem  22534  ig1peu  22657  ig1pdvds  22662  taylfvallem1  22837  tayl0  22842  taylply2  22848  taylply  22849  dvtaylp  22850  dvntaylp  22851  dvntaylp0  22852  taylthlem1  22853  ulmdvlem1  22880  ulmdvlem3  22882  psercn  22906  pserdvlem2  22908  abelth  22921  xrlimcnp  23415  wilthlem2  23460  sqff1o  23573  chtublem  23603  pntlemq  23903  pntlemf  23907  tglineintmo  24142  ttgcontlem1  24309  ghsubgolemOLD  25489  shintcli  26364  shub1  26417  mdslmd1lem1  27360  mdexchi  27370  chirredlem1  27425  mdsymlem5  27442  sumdmdii  27450  sumdmdlem2  27454  xrsupssd  27729  xrge0infssd  27731  xrge0tsmsd  27929  locfinreflem  27997  cmpcref  28007  pnfneige0  28087  esum2d  28241  insiga  28286  sssigagen2  28295  dya2iocnei  28409  omsmon  28425  carsgclctunlem1  28444  carsggect  28445  omsmeas  28450  lgamucov  28769  erdszelem7  28830  erdszelem8  28831  erdsze2lem1  28836  conpcon  28869  cvmliftmolem1  28915  cvmlift2lem1  28936  cvmlift2lem9  28945  cvmlift2lem10  28946  cvmlift3lem6  28958  cvmlift3lem7  28959  ss2mcls  29117  dftrpred3g  29481  nofulllem3  29629  ontgval  30049  opnmbllem0  30215  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  neibastop2lem  30344  fnemeet2  30351  fnejoin1  30352  sstotbnd2  30436  heiborlem1  30473  heiborlem8  30480  intidl  30592  elrfi  30792  ismrcd1  30796  istopclsd  30798  mrefg2  30805  aomclem2  31167  aomclem6  31171  hbtlem6  31246  hbt  31247  limccog  31792  limclner  31823  cncfmptssg  31838  cncfuni  31855  icccncfext  31856  dvresntr  31879  dvmptresicc  31882  dvbdfbdioolem1  31891  dvdmsscn  31899  dvnxpaek  31905  dvnprodlem2  31910  stoweidlem59  32007  fourierdlem20  32075  fourierdlem42  32097  fourierdlem48  32103  fourierdlem49  32104  fourierdlem52  32107  fourierdlem58  32113  fourierdlem64  32119  fourierdlem73  32128  fourierdlem76  32131  fourierdlem80  32135  fourierdlem84  32139  fourierdlem93  32148  fourierdlem103  32158  fourierdlem104  32159  fourierdlem113  32168  etransclem18  32201  subsubmgm  32803  bnj906  34335  bnj1020  34368  bnj1137  34398  bnj1408  34439  bnj1452  34455  lsmsat  35146  lssats  35150  lpssat  35151  lssatle  35153  lssat  35154  lsatcvatlem  35187  paddss12  35956  paddasslem17  35973  pmodlem1  35983  pmod1i  35985  pmodl42N  35988  elpcliN  36030  pclfinN  36037  polcon3N  36054  polcon2N  36056  paddunN  36064  pclfinclN  36087  poml5N  36091  osumcllem1N  36093  osumcllem2N  36094  osumcllem3N  36095  pl42lem2N  36117  pl42lem4N  36119  cdlemn5pre  37340  dihord1  37358  dihord2a  37359  dihord2b  37360  dihord5b  37399  dochss  37505  dochdmj1  37530  djhsumss  37547  djhunssN  37549  dochexmidlem2  37601  lclkrslem1  37677  lclkrslem2  37678  lcfrlem2  37683  dfrcl2  38211  relexp0a  38241  trclimalb2  38257  imo72b2lem0  38511  imo72b2lem2  38513  imo72b2lem1  38517  imo72b2  38522
  Copyright terms: Public domain W3C validator