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

Theorem sstrd 3361
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 3359 . 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 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  syl5ss  3362  syl6ss  3363  ssdif2d  3490  uniintsn  4160  funss  5431  fssxp  5565  knatar  6043  suppssfvOLD  6311  suppssov1OLD  6312  tfisi  6464  suppfnss  6709  suppssov1  6716  suppssfv  6720  tposss  6741  tfrlem1  6827  omwordri  7003  oewordri  7023  oeeui  7033  oaabs2  7076  omopthlem1  7086  ecinxp  7167  sbthlem1  7413  dffi2  7665  hartogslem1  7748  cantnfcl  7867  cantnflt  7872  cantnfp1lem3  7880  cantnflem3  7891  cantnfclOLD  7897  cantnfltOLD  7902  cantnfp1lem3OLD  7906  cantnflem3OLD  7913  cnfcom  7925  cnfcom3lem  7928  cnfcomOLD  7933  cnfcom3lemOLD  7936  rankssb  8047  tskwe  8112  dfac12lem2  8305  dfac12lem3  8306  cfflb  8420  cfcof  8435  ssfin2  8481  hsmexlem4  8590  ttukeylem6  8675  ttukeylem7  8676  fpwwe2lem1  8790  fpwwe2lem8  8796  fpwwe2lem11  8799  fpwwe2lem12  8800  canthnumlem  8807  canthwelem  8809  canthwe  8810  canthp1lem2  8812  pwfseqlem5  8822  wunex2  8897  tsktrss  8920  inttsk  8933  uzwo3  10940  supicc  11425  supiccub  11426  supicclub  11427  seqsplit  11831  seqf1olem2a  11836  seqz  11846  swrdval2  12308  sumss  13193  qshash  13282  incexc  13292  incexc2  13293  rpnnen2lem11  13499  vdwlem1  14034  ramub1lem1  14079  imasaddvallem  14459  imasvscaf  14469  mrerintcl  14527  ismred2  14533  mremre  14534  mrcuni  14551  mressmrcd  14557  submrc  14558  mrissmrid  14571  mreexexlem2d  14575  isacs2  14583  isacs1i  14587  invss  14691  ssctr  14730  funcres2b  14799  isacs3lem  15328  acsfiindd  15339  acsmapd  15340  acsmap2d  15341  tsrdir  15400  subsubm  15476  gsumwspan  15515  subsubg  15695  subgint  15696  cntzidss  15846  symggen  15967  pmtrdifellem1  15973  pmtrdifellem2  15974  pgpssslw  16104  lsmless1x  16134  lsmless2x  16135  lsmless12  16151  subglsm  16161  gsumval3OLD  16373  gsumval3lem2  16375  gsumzaddlem  16399  gsumzadd  16400  gsumzaddOLD  16402  gsumconst  16417  gsum2d  16451  gsum2dOLD  16452  dmdprdd  16469  dprdfeq0  16500  dprdfeq0OLD  16507  dprdspan  16512  dprdres  16513  dprdss  16514  dprdz  16515  subgdmdprd  16519  subgdprd  16520  dprdsn  16521  dprd2dlem1  16528  dprd2da  16529  dmdprdsplit2lem  16532  dprdsplit  16535  pgpfac1lem2  16564  pgpfac1lem3  16566  pgpfac1lem5  16568  subsubrg  16869  lspss  17042  lspun  17045  lsslsp  17073  lmhmlsp  17107  lsmelval2  17143  lsmssspx  17146  lsppratlem2  17206  lsppratlem3  17207  lsppratlem4  17208  lbsextlem2  17217  lbsextlem3  17218  aspss  17380  ocvlsp  18076  cssmre  18093  obselocv  18128  obslbs  18130  toponmre  18672  neiint  18683  neiss  18688  lpss  18721  lpss3  18723  restopnb  18754  restfpw  18758  neitr  18759  restcls  18760  restntr  18761  restlp  18762  ordtbas  18771  pnfnei  18799  mnfnei  18800  iscnp4  18842  cnclsi  18851  isreg2  18956  discmp  18976  cmpcld  18980  uncmp  18981  sscmp  18983  hauscmplem  18984  cmpfi  18986  iunconlem  19006  clscon  19009  2ndcctbss  19034  restnlly  19061  llyrest  19064  nllyrest  19065  llyidm  19067  nllyidm  19068  cldllycmp  19074  dislly  19076  llycmpkgen2  19098  ptbasfi  19129  txnlly  19185  txcmplem1  19189  tx1stc  19198  xkococnlem  19207  qtopval2  19244  basqtop  19259  tgqtop  19260  qtoprest  19265  kqreglem1  19289  kqreglem2  19290  kqnrmlem1  19291  kqnrmlem2  19292  fsubbas  19415  fgabs  19427  fbasrn  19432  trfil2  19435  trfg  19439  isufil2  19456  trufil  19458  ssufl  19466  ufileu  19467  filufint  19468  fmfnfmlem4  19505  fmfnfm  19506  flimss2  19520  flimss1  19521  fclsfnflim  19575  flimfnfcls  19576  fclscmp  19578  cnpfcfi  19588  alexsubALT  19598  clssubg  19654  clsnsg  19655  tsmsres  19693  ustexsym  19765  ustex2sym  19766  ustex3sym  19767  ustund  19771  ustneism  19773  trust  19779  utoptop  19784  restutopopn  19788  utop2nei  19800  utopreg  19802  cfiluweak  19845  neipcfilu  19846  blssps  19974  blss  19975  blcld  20055  blsscls  20057  met1stc  20071  met2ndci  20072  metustOLD  20117  metust  20118  cfilucfilOLD  20119  cfilucfil  20120  restmetu  20137  tgqioo  20352  xrsblre  20363  reconnlem2  20379  xrge0gsumle  20385  xrge0tsms  20386  rescncf  20448  cnmpt2pc  20475  cnheibor  20502  cnllycmp  20503  lebnum  20511  phtpycn  20530  cfilfcls  20760  iscmet3lem2  20778  cmetss  20800  cncmet  20808  bcthlem4  20813  bcth3  20817  rrxcph  20871  rrxmetlem  20881  minveclem4a  20892  minveclem4  20894  ivthicc  20917  ovollb  20937  ovollb2lem  20946  ovollb2  20947  nulmbl2  20993  ioorcl2  21027  uniioombllem3  21040  uniioombllem4  21041  uniioombllem5  21042  opnmbllem  21056  volcn  21061  volivth  21062  mbfeqalem  21095  itg10a  21163  mbfi1fseqlem4  21171  ditgcl  21308  ditgswap  21309  ditgsplitlem  21310  limcflf  21331  limcres  21336  dvbss  21351  dvbsss  21352  perfdvf  21353  dvreslem  21359  dvres2lem  21360  dvres3  21363  dvcnp  21368  dvcnp2  21369  dvcn  21370  dvnff  21372  dvn2bss  21379  dvnres  21380  cpnord  21384  dvaddbr  21387  dvmulbr  21388  dvcobr  21395  dvnfre  21401  dvmptres2  21411  dvmptntr  21420  dvcnvlem  21423  dvcnv  21424  dvferm1lem  21431  dvferm2lem  21433  dvlip  21440  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  dvgt0lem1  21449  lhop1lem  21460  lhop  21463  dvcnvrelem1  21464  dvcnvrelem2  21465  dvcnvre  21466  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  ftc1lem1  21482  ftc1lem2  21483  ftc1a  21484  ftc1lem4  21486  ftc2ditglem  21492  itgsubstlem  21495  ig1peu  21618  ig1pdvds  21623  taylfvallem1  21797  tayl0  21802  taylply2  21808  taylply  21809  dvtaylp  21810  dvntaylp  21811  dvntaylp0  21812  taylthlem1  21813  ulmdvlem1  21840  ulmdvlem3  21842  psercn  21866  pserdvlem2  21868  abelth  21881  xrlimcnp  22337  wilthlem2  22382  sqff1o  22495  chtublem  22525  pntlemq  22825  pntlemf  22829  tglineintmo  23016  ttgcontlem1  23082  ghsubgolem  23808  shintcli  24683  shub1  24736  mdslmd1lem1  25680  mdexchi  25690  chirredlem1  25745  mdsymlem5  25762  sumdmdii  25770  sumdmdlem2  25774  ofpreima2  25936  xrsupssd  26003  xrge0infssd  26005  xrge0tsmsd  26204  pnfneige0  26333  insiga  26532  sssigagen2  26541  dya2iocnei  26649  omsmon  26663  lgamucov  26976  erdszelem7  27037  erdszelem8  27038  erdsze2lem1  27043  conpcon  27076  cvmliftmolem1  27122  cvmlift2lem1  27143  cvmlift2lem9  27152  cvmlift2lem10  27153  cvmlift3lem6  27165  cvmlift3lem7  27166  rtrclreclem.min  27300  prodss  27411  dftrpred3g  27648  nofulllem3  27796  ontgval  28229  opnmbllem0  28380  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  comppfsc  28532  neibastop2lem  28534  fnemeet2  28541  fnejoin1  28542  sstotbnd2  28626  heiborlem1  28663  heiborlem8  28670  intidl  28782  elrfi  28983  ismrcd1  28987  istopclsd  28989  mrefg2  28996  aomclem2  29361  aomclem6  29365  hbtlem6  29438  hbt  29439  stoweidlem59  29807  bnj906  31810  bnj1020  31843  bnj1137  31873  bnj1408  31914  bnj1452  31930  lsmsat  32493  lssats  32497  lpssat  32498  lssatle  32500  lssat  32501  lsatcvatlem  32534  paddss12  33303  paddasslem17  33320  pmodlem1  33330  pmod1i  33332  pmodl42N  33335  elpcliN  33377  pclfinN  33384  polcon3N  33401  polcon2N  33403  paddunN  33411  pclfinclN  33434  poml5N  33438  osumcllem1N  33440  osumcllem2N  33441  osumcllem3N  33442  pl42lem2N  33464  pl42lem4N  33466  cdlemn5pre  34685  dihord1  34703  dihord2a  34704  dihord2b  34705  dihord5b  34744  dochss  34850  dochdmj1  34875  djhsumss  34892  djhunssN  34894  dochexmidlem2  34946  lclkrslem1  35022  lclkrslem2  35023  lcfrlem2  35028
  Copyright terms: Public domain W3C validator