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

Theorem sstrd 3354
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 3352 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 654 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  syl5ss  3355  syl6ss  3356  ssdif2d  3483  uniintsn  4153  funss  5424  fssxp  5558  knatar  6035  suppssfvOLD  6305  suppssov1OLD  6306  tfisi  6458  suppfnss  6703  suppssov1  6710  suppssfv  6714  tposss  6735  tfrlem1  6821  omwordri  6999  oewordri  7019  oeeui  7029  oaabs2  7072  omopthlem1  7082  ecinxp  7163  sbthlem1  7409  dffi2  7661  hartogslem1  7744  cantnfcl  7863  cantnflt  7868  cantnfp1lem3  7876  cantnflem3  7887  cantnfclOLD  7893  cantnfltOLD  7898  cantnfp1lem3OLD  7902  cantnflem3OLD  7909  cnfcom  7921  cnfcom3lem  7924  cnfcomOLD  7929  cnfcom3lemOLD  7932  rankssb  8043  tskwe  8108  dfac12lem2  8301  dfac12lem3  8302  cfflb  8416  cfcof  8431  ssfin2  8477  hsmexlem4  8586  ttukeylem6  8671  ttukeylem7  8672  fpwwe2lem1  8786  fpwwe2lem8  8792  fpwwe2lem11  8795  fpwwe2lem12  8796  canthnumlem  8803  canthwelem  8805  canthwe  8806  canthp1lem2  8808  pwfseqlem5  8818  wunex2  8893  tsktrss  8916  inttsk  8929  uzwo3  10936  supicc  11420  supiccub  11421  supicclub  11422  seqsplit  11823  seqf1olem2a  11828  seqz  11838  swrdval2  12300  sumss  13185  qshash  13273  incexc  13283  incexc2  13284  rpnnen2lem11  13490  vdwlem1  14025  ramub1lem1  14070  imasaddvallem  14450  imasvscaf  14460  mrerintcl  14518  ismred2  14524  mremre  14525  mrcuni  14542  mressmrcd  14548  submrc  14549  mrissmrid  14562  mreexexlem2d  14566  isacs2  14574  isacs1i  14578  invss  14682  ssctr  14721  funcres2b  14790  isacs3lem  15319  acsfiindd  15330  acsmapd  15331  acsmap2d  15332  tsrdir  15391  subsubm  15467  gsumwspan  15504  subsubg  15684  subgint  15685  cntzidss  15835  symggen  15956  pmtrdifellem1  15962  pmtrdifellem2  15963  pgpssslw  16093  lsmless1x  16123  lsmless2x  16124  lsmless12  16140  subglsm  16150  gsumval3OLD  16362  gsumval3lem2  16364  gsumzaddlem  16388  gsumzadd  16389  gsumzaddOLD  16391  gsumconst  16406  gsum2d  16437  gsum2dOLD  16438  dmdprdd  16455  dprdfeq0  16486  dprdfeq0OLD  16493  dprdspan  16498  dprdres  16499  dprdss  16500  dprdz  16501  subgdmdprd  16505  subgdprd  16506  dprdsn  16507  dprd2dlem1  16514  dprd2da  16515  dmdprdsplit2lem  16518  dprdsplit  16521  pgpfac1lem2  16550  pgpfac1lem3  16552  pgpfac1lem5  16554  subsubrg  16815  lspss  16987  lspun  16990  lsslsp  17018  lmhmlsp  17052  lsmelval2  17088  lsmssspx  17091  lsppratlem2  17151  lsppratlem3  17152  lsppratlem4  17153  lbsextlem2  17162  lbsextlem3  17163  aspss  17325  ocvlsp  17943  cssmre  17960  obselocv  17995  obslbs  17997  toponmre  18539  neiint  18550  neiss  18555  lpss  18588  lpss3  18590  restopnb  18621  restfpw  18625  neitr  18626  restcls  18627  restntr  18628  restlp  18629  ordtbas  18638  pnfnei  18666  mnfnei  18667  iscnp4  18709  cnclsi  18718  isreg2  18823  discmp  18843  cmpcld  18847  uncmp  18848  sscmp  18850  hauscmplem  18851  cmpfi  18853  iunconlem  18873  clscon  18876  2ndcctbss  18901  restnlly  18928  llyrest  18931  nllyrest  18932  llyidm  18934  nllyidm  18935  cldllycmp  18941  dislly  18943  llycmpkgen2  18965  ptbasfi  18996  txnlly  19052  txcmplem1  19056  tx1stc  19065  xkococnlem  19074  qtopval2  19111  basqtop  19126  tgqtop  19127  qtoprest  19132  kqreglem1  19156  kqreglem2  19157  kqnrmlem1  19158  kqnrmlem2  19159  fsubbas  19282  fgabs  19294  fbasrn  19299  trfil2  19302  trfg  19306  isufil2  19323  trufil  19325  ssufl  19333  ufileu  19334  filufint  19335  fmfnfmlem4  19372  fmfnfm  19373  flimss2  19387  flimss1  19388  fclsfnflim  19442  flimfnfcls  19443  fclscmp  19445  cnpfcfi  19455  alexsubALT  19465  clssubg  19521  clsnsg  19522  tsmsres  19560  ustexsym  19632  ustex2sym  19633  ustex3sym  19634  ustund  19638  ustneism  19640  trust  19646  utoptop  19651  restutopopn  19655  utop2nei  19667  utopreg  19669  cfiluweak  19712  neipcfilu  19713  blssps  19841  blss  19842  blcld  19922  blsscls  19924  met1stc  19938  met2ndci  19939  metustOLD  19984  metust  19985  cfilucfilOLD  19986  cfilucfil  19987  restmetu  20004  tgqioo  20219  xrsblre  20230  reconnlem2  20246  xrge0gsumle  20252  xrge0tsms  20253  rescncf  20315  cnmpt2pc  20342  cnheibor  20369  cnllycmp  20370  lebnum  20378  phtpycn  20397  cfilfcls  20627  iscmet3lem2  20645  cmetss  20667  cncmet  20675  bcthlem4  20680  bcth3  20684  rrxcph  20738  rrxmetlem  20748  minveclem4a  20759  minveclem4  20761  ivthicc  20784  ovollb  20804  ovollb2lem  20813  ovollb2  20814  nulmbl2  20860  ioorcl2  20894  uniioombllem3  20907  uniioombllem4  20908  uniioombllem5  20909  opnmbllem  20923  volcn  20928  volivth  20929  mbfeqalem  20962  itg10a  21030  mbfi1fseqlem4  21038  ditgcl  21175  ditgswap  21176  ditgsplitlem  21177  limcflf  21198  limcres  21203  dvbss  21218  dvbsss  21219  perfdvf  21220  dvreslem  21226  dvres2lem  21227  dvres3  21230  dvcnp  21235  dvcnp2  21236  dvcn  21237  dvnff  21239  dvn2bss  21246  dvnres  21247  cpnord  21251  dvaddbr  21254  dvmulbr  21255  dvcobr  21262  dvnfre  21268  dvmptres2  21278  dvmptntr  21287  dvcnvlem  21290  dvcnv  21291  dvferm1lem  21298  dvferm2lem  21300  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  dvgt0lem1  21316  lhop1lem  21327  lhop  21330  dvcnvrelem1  21331  dvcnvrelem2  21332  dvcnvre  21333  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  ftc1lem1  21349  ftc1lem2  21350  ftc1a  21351  ftc1lem4  21353  ftc2ditglem  21359  itgsubstlem  21362  ig1peu  21528  ig1pdvds  21533  taylfvallem1  21707  tayl0  21712  taylply2  21718  taylply  21719  dvtaylp  21720  dvntaylp  21721  dvntaylp0  21722  taylthlem1  21723  ulmdvlem1  21750  ulmdvlem3  21752  psercn  21776  pserdvlem2  21778  abelth  21791  xrlimcnp  22247  wilthlem2  22292  sqff1o  22405  chtublem  22435  pntlemq  22735  pntlemf  22739  tglineintmo  22917  ttgcontlem1  22954  ghsubgolem  23680  shintcli  24555  shub1  24608  mdslmd1lem1  25552  mdexchi  25562  chirredlem1  25617  mdsymlem5  25634  sumdmdii  25642  sumdmdlem2  25646  ofpreima2  25809  xrsupssd  25877  xrge0tsmsd  26106  pnfneige0  26235  insiga  26434  sssigagen2  26443  dya2iocnei  26551  lgamucov  26872  erdszelem7  26933  erdszelem8  26934  erdsze2lem1  26939  conpcon  26972  cvmliftmolem1  27018  cvmlift2lem1  27039  cvmlift2lem9  27048  cvmlift2lem10  27049  cvmlift3lem6  27061  cvmlift3lem7  27062  rtrclreclem.min  27196  prodss  27307  dftrpred3g  27544  nofulllem3  27692  ontgval  28125  opnmbllem0  28271  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  comppfsc  28423  neibastop2lem  28425  fnemeet2  28432  fnejoin1  28433  sstotbnd2  28517  heiborlem1  28554  heiborlem8  28561  intidl  28673  elrfi  28875  ismrcd1  28879  istopclsd  28881  mrefg2  28888  aomclem2  29253  aomclem6  29257  hbtlem6  29330  hbt  29331  stoweidlem59  29700  bnj906  31625  bnj1020  31658  bnj1137  31688  bnj1408  31729  bnj1452  31745  lsmsat  32226  lssats  32230  lpssat  32231  lssatle  32233  lssat  32234  lsatcvatlem  32267  paddss12  33036  paddasslem17  33053  pmodlem1  33063  pmod1i  33065  pmodl42N  33068  elpcliN  33110  pclfinN  33117  polcon3N  33134  polcon2N  33136  paddunN  33144  pclfinclN  33167  poml5N  33171  osumcllem1N  33173  osumcllem2N  33174  osumcllem3N  33175  pl42lem2N  33197  pl42lem4N  33199  cdlemn5pre  34418  dihord1  34436  dihord2a  34437  dihord2b  34438  dihord5b  34477  dochss  34583  dochdmj1  34608  djhsumss  34625  djhunssN  34627  dochexmidlem2  34679  lclkrslem1  34755  lclkrslem2  34756  lcfrlem2  34761
  Copyright terms: Public domain W3C validator