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

Theorem sstrd 3475
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 3473 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3444  df-ss 3451
This theorem is referenced by:  syl5ss  3476  syl6ss  3477  ssdif2d  3604  uniintsn  4274  funss  5545  fssxp  5679  knatar  6158  suppssfvOLD  6427  suppssov1OLD  6428  tfisi  6580  suppfnss  6825  suppssov1  6832  suppssfv  6836  tposss  6857  tfrlem1  6946  omwordri  7122  oewordri  7142  oeeui  7152  oaabs2  7195  omopthlem1  7205  ecinxp  7286  sbthlem1  7532  dffi2  7785  hartogslem1  7868  cantnfcl  7987  cantnflt  7992  cantnfp1lem3  8000  cantnflem3  8011  cantnfclOLD  8017  cantnfltOLD  8022  cantnfp1lem3OLD  8026  cantnflem3OLD  8033  cnfcom  8045  cnfcom3lem  8048  cnfcomOLD  8053  cnfcom3lemOLD  8056  rankssb  8167  tskwe  8232  dfac12lem2  8425  dfac12lem3  8426  cfflb  8540  cfcof  8555  ssfin2  8601  hsmexlem4  8710  ttukeylem6  8795  ttukeylem7  8796  fpwwe2lem1  8910  fpwwe2lem8  8916  fpwwe2lem11  8919  fpwwe2lem12  8920  canthnumlem  8927  canthwelem  8929  canthwe  8930  canthp1lem2  8932  pwfseqlem5  8942  wunex2  9017  tsktrss  9040  inttsk  9053  uzwo3  11060  supicc  11551  supiccub  11552  supicclub  11553  seqsplit  11957  seqf1olem2a  11962  seqz  11972  swrdval2  12435  sumss  13320  qshash  13409  incexc  13419  incexc2  13420  rpnnen2lem11  13626  vdwlem1  14161  ramub1lem1  14206  imasaddvallem  14587  imasvscaf  14597  mrerintcl  14655  ismred2  14661  mremre  14662  mrcuni  14679  mressmrcd  14685  submrc  14686  mrissmrid  14699  mreexexlem2d  14703  isacs2  14711  isacs1i  14715  invss  14819  ssctr  14858  funcres2b  14927  isacs3lem  15456  acsfiindd  15467  acsmapd  15468  acsmap2d  15469  tsrdir  15528  subsubm  15605  gsumwspan  15644  subsubg  15824  subgint  15825  cntzidss  15975  symggen  16096  pmtrdifellem1  16102  pmtrdifellem2  16103  pgpssslw  16235  lsmless1x  16265  lsmless2x  16266  lsmless12  16282  subglsm  16292  gsumval3OLD  16504  gsumval3lem2  16506  gsumzaddlem  16530  gsumzadd  16531  gsumzaddOLD  16533  gsumconst  16550  gsum2d  16586  gsum2dOLD  16587  dmdprdd  16604  dprdfeq0  16635  dprdfeq0OLD  16642  dprdspan  16647  dprdres  16648  dprdss  16649  dprdz  16650  subgdmdprd  16654  subgdprd  16655  dprdsn  16656  dprd2dlem1  16663  dprd2da  16664  dmdprdsplit2lem  16667  dprdsplit  16670  pgpfac1lem2  16699  pgpfac1lem3  16701  pgpfac1lem5  16703  subsubrg  17015  lspss  17189  lspun  17192  lsslsp  17220  lmhmlsp  17254  lsmelval2  17290  lsmssspx  17293  lsppratlem2  17353  lsppratlem3  17354  lsppratlem4  17355  lbsextlem2  17364  lbsextlem3  17365  aspss  17527  ocvlsp  18227  cssmre  18244  obselocv  18279  obslbs  18281  toponmre  18830  neiint  18841  neiss  18846  lpss  18879  lpss3  18881  restopnb  18912  restfpw  18916  neitr  18917  restcls  18918  restntr  18919  restlp  18920  ordtbas  18929  pnfnei  18957  mnfnei  18958  iscnp4  19000  cnclsi  19009  isreg2  19114  discmp  19134  cmpcld  19138  uncmp  19139  sscmp  19141  hauscmplem  19142  cmpfi  19144  iunconlem  19164  clscon  19167  2ndcctbss  19192  restnlly  19219  llyrest  19222  nllyrest  19223  llyidm  19225  nllyidm  19226  cldllycmp  19232  dislly  19234  llycmpkgen2  19256  ptbasfi  19287  txnlly  19343  txcmplem1  19347  tx1stc  19356  xkococnlem  19365  qtopval2  19402  basqtop  19417  tgqtop  19418  qtoprest  19423  kqreglem1  19447  kqreglem2  19448  kqnrmlem1  19449  kqnrmlem2  19450  fsubbas  19573  fgabs  19585  fbasrn  19590  trfil2  19593  trfg  19597  isufil2  19614  trufil  19616  ssufl  19624  ufileu  19625  filufint  19626  fmfnfmlem4  19663  fmfnfm  19664  flimss2  19678  flimss1  19679  fclsfnflim  19733  flimfnfcls  19734  fclscmp  19736  cnpfcfi  19746  alexsubALT  19756  clssubg  19812  clsnsg  19813  tsmsres  19851  ustexsym  19923  ustex2sym  19924  ustex3sym  19925  ustund  19929  ustneism  19931  trust  19937  utoptop  19942  restutopopn  19946  utop2nei  19958  utopreg  19960  cfiluweak  20003  neipcfilu  20004  blssps  20132  blss  20133  blcld  20213  blsscls  20215  met1stc  20229  met2ndci  20230  metustOLD  20275  metust  20276  cfilucfilOLD  20277  cfilucfil  20278  restmetu  20295  tgqioo  20510  xrsblre  20521  reconnlem2  20537  xrge0gsumle  20543  xrge0tsms  20544  rescncf  20606  cnmpt2pc  20633  cnheibor  20660  cnllycmp  20661  lebnum  20669  phtpycn  20688  cfilfcls  20918  iscmet3lem2  20936  cmetss  20958  cncmet  20966  bcthlem4  20971  bcth3  20975  rrxcph  21029  rrxmetlem  21039  minveclem4a  21050  minveclem4  21052  ivthicc  21075  ovollb  21095  ovollb2lem  21104  ovollb2  21105  nulmbl2  21152  ioorcl2  21186  uniioombllem3  21199  uniioombllem4  21200  uniioombllem5  21201  opnmbllem  21215  volcn  21220  volivth  21221  mbfeqalem  21254  itg10a  21322  mbfi1fseqlem4  21330  ditgcl  21467  ditgswap  21468  ditgsplitlem  21469  limcflf  21490  limcres  21495  dvbss  21510  dvbsss  21511  perfdvf  21512  dvreslem  21518  dvres2lem  21519  dvres3  21522  dvcnp  21527  dvcnp2  21528  dvcn  21529  dvnff  21531  dvn2bss  21538  dvnres  21539  cpnord  21543  dvaddbr  21546  dvmulbr  21547  dvcobr  21554  dvnfre  21560  dvmptres2  21570  dvmptntr  21579  dvcnvlem  21582  dvcnv  21583  dvferm1lem  21590  dvferm2lem  21592  dvlip  21599  dvlipcn  21600  dvlip2  21601  c1liplem1  21602  dvgt0lem1  21608  lhop1lem  21619  lhop  21622  dvcnvrelem1  21623  dvcnvrelem2  21624  dvcnvre  21625  dvfsumle  21627  dvfsumge  21628  dvfsumabs  21629  ftc1lem1  21641  ftc1lem2  21642  ftc1a  21643  ftc1lem4  21645  ftc2ditglem  21651  itgsubstlem  21654  ig1peu  21777  ig1pdvds  21782  taylfvallem1  21956  tayl0  21961  taylply2  21967  taylply  21968  dvtaylp  21969  dvntaylp  21970  dvntaylp0  21971  taylthlem1  21972  ulmdvlem1  21999  ulmdvlem3  22001  psercn  22025  pserdvlem2  22027  abelth  22040  xrlimcnp  22496  wilthlem2  22541  sqff1o  22654  chtublem  22684  pntlemq  22984  pntlemf  22988  tglineintmo  23187  ttgcontlem1  23284  ghsubgolem  24010  shintcli  24885  shub1  24938  mdslmd1lem1  25882  mdexchi  25892  chirredlem1  25947  mdsymlem5  25964  sumdmdii  25972  sumdmdlem2  25976  ofpreima2  26137  xrsupssd  26204  xrge0infssd  26206  xrge0tsmsd  26399  pnfneige0  26527  insiga  26726  sssigagen2  26735  dya2iocnei  26842  omsmon  26856  lgamucov  27169  erdszelem7  27230  erdszelem8  27231  erdsze2lem1  27236  conpcon  27269  cvmliftmolem1  27315  cvmlift2lem1  27336  cvmlift2lem9  27345  cvmlift2lem10  27346  cvmlift3lem6  27358  cvmlift3lem7  27359  rtrclreclem.min  27494  prodss  27605  dftrpred3g  27842  nofulllem3  27990  ontgval  28422  opnmbllem0  28576  ftc1anclem7  28622  ftc1anclem8  28623  ftc1anc  28624  comppfsc  28728  neibastop2lem  28730  fnemeet2  28737  fnejoin1  28738  sstotbnd2  28822  heiborlem1  28859  heiborlem8  28866  intidl  28978  elrfi  29179  ismrcd1  29183  istopclsd  29185  mrefg2  29192  aomclem2  29557  aomclem6  29561  hbtlem6  29634  hbt  29635  stoweidlem59  30003  bnj906  32256  bnj1020  32289  bnj1137  32319  bnj1408  32360  bnj1452  32376  lsmsat  32992  lssats  32996  lpssat  32997  lssatle  32999  lssat  33000  lsatcvatlem  33033  paddss12  33802  paddasslem17  33819  pmodlem1  33829  pmod1i  33831  pmodl42N  33834  elpcliN  33876  pclfinN  33883  polcon3N  33900  polcon2N  33902  paddunN  33910  pclfinclN  33933  poml5N  33937  osumcllem1N  33939  osumcllem2N  33940  osumcllem3N  33941  pl42lem2N  33963  pl42lem4N  33965  cdlemn5pre  35184  dihord1  35202  dihord2a  35203  dihord2b  35204  dihord5b  35243  dochss  35349  dochdmj1  35374  djhsumss  35391  djhunssN  35393  dochexmidlem2  35445  lclkrslem1  35521  lclkrslem2  35522  lcfrlem2  35527
  Copyright terms: Public domain W3C validator