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

Theorem sstrd 3191
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 3189 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3154
This theorem is referenced by:  syl5ss  3192  syl6ss  3193  ssdif2d  3317  uniintsn  3901  tfisi  4651  funss  5275  fssxp  5402  knatar  5859  suppssfv  6076  suppssov1  6077  tposss  6237  omwordri  6572  oewordri  6592  oeeui  6602  oaabs2  6645  omopthlem1  6655  ecinxp  6736  sbthlem1  6973  dffi2  7178  hartogslem1  7259  cantnfcl  7370  cantnflt  7375  cantnfp1lem3  7384  cantnflem3  7395  cnfcom  7405  cnfcom3lem  7408  rankssb  7522  tskwe  7585  dfac12lem2  7772  dfac12lem3  7773  cfflb  7887  cfcof  7902  ssfin2  7948  hsmexlem4  8057  ttukeylem6  8143  ttukeylem7  8144  fpwwe2lem1  8255  fpwwe2lem8  8261  fpwwe2lem11  8264  fpwwe2lem12  8265  canthnumlem  8272  canthwelem  8274  canthwe  8275  canthp1lem2  8277  pwfseqlem5  8287  wunex2  8362  tsktrss  8385  inttsk  8398  uzwo3  10313  seqsplit  11081  seqf1olem2a  11086  seqz  11096  swrdval2  11455  sumss  12199  qshash  12287  incexc  12298  incexc2  12299  rpnnen2lem11  12505  vdwlem1  13030  ramub1lem1  13075  imasaddvallem  13433  imasvscaf  13443  mrerintcl  13501  ismred2  13507  mremre  13508  mrcuni  13525  mressmrcd  13531  submrc  13532  mrissmrid  13545  mreexexlem2d  13549  isacs2  13557  isacs1i  13561  invss  13665  ssctr  13704  funcres2b  13773  isacs3lem  14271  acsfiindd  14282  acsmapd  14283  acsmap2d  14284  tsrdir  14362  subsubm  14436  gsumwspan  14470  subsubg  14642  subgint  14643  cntzidss  14815  pgpssslw  14927  lsmless1x  14957  lsmless2x  14958  lsmless12  14974  subglsm  14984  gsumval3  15193  gsumzadd  15206  gsum2d  15225  dmdprdd  15239  dprdfeq0  15259  dprdspan  15264  dprdres  15265  dprdss  15266  dprdz  15267  subgdmdprd  15271  subgdprd  15272  dprdsn  15273  dprd2dlem1  15278  dprd2da  15279  dmdprdsplit2lem  15282  dprdsplit  15285  pgpfac1lem2  15312  pgpfac1lem3  15314  pgpfac1lem5  15316  subsubrg  15573  lspss  15743  lspun  15746  lsslsp  15774  lmhmlsp  15808  lsmelval2  15840  lsmssspx  15843  lsppratlem2  15903  lsppratlem3  15904  lsppratlem4  15905  lbsextlem2  15914  lbsextlem3  15915  aspss  16074  ocvlsp  16578  cssmre  16595  obselocv  16630  obslbs  16632  toponmre  16832  neiint  16843  neiss  16848  lpss  16876  lpss3  16878  restopnb  16908  restfpw  16912  restcls  16913  restntr  16914  restlp  16915  ordtbas  16924  pnfnei  16952  mnfnei  16953  cnclsi  17003  isreg2  17107  discmp  17127  cmpcld  17131  uncmp  17132  sscmp  17134  hauscmplem  17135  cmpfi  17137  iunconlem  17155  clscon  17158  2ndcctbss  17183  restnlly  17210  llyrest  17213  nllyrest  17214  llyidm  17216  nllyidm  17217  cldllycmp  17223  dislly  17225  llycmpkgen2  17247  ptbasfi  17278  txnlly  17333  txcmplem1  17337  tx1stc  17346  xkococnlem  17355  qtopval2  17389  basqtop  17404  tgqtop  17405  qtoprest  17410  kqreglem1  17434  kqreglem2  17435  kqnrmlem1  17436  kqnrmlem2  17437  fsubbas  17564  fgabs  17576  fbasrn  17581  trfil2  17584  trfg  17588  isufil2  17605  trufil  17607  ssufl  17615  ufileu  17616  filufint  17617  fmfnfmlem4  17654  fmfnfm  17655  flimss2  17669  flimss1  17670  fclsfnflim  17724  flimfnfcls  17725  fclscmp  17727  cnpfcfi  17737  alexsubALT  17747  clssubg  17793  clsnsg  17794  blss  17974  blcld  18053  blsscls  18055  met1stc  18069  met2ndci  18070  tgqioo  18308  xrsblre  18319  reconnlem2  18334  xrge0gsumle  18340  xrge0tsms  18341  rescncf  18403  cnmpt2pc  18428  cnheibor  18455  cnllycmp  18456  lebnum  18464  phtpycn  18483  cfilfcls  18702  iscmet3lem2  18720  cmetss  18742  cncmet  18746  bcthlem4  18751  bcth3  18755  minveclem4a  18796  minveclem4  18798  ivthicc  18820  ovollb  18840  ovollb2lem  18849  ovollb2  18850  nulmbl2  18896  ioorcl2  18929  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  opnmbllem  18958  volcn  18963  volivth  18964  mbfeqalem  18999  itg10a  19067  mbfi1fseqlem4  19075  ditgcl  19210  ditgswap  19211  ditgsplitlem  19212  limcflf  19233  limcres  19238  dvbss  19253  dvbsss  19254  perfdvf  19255  dvreslem  19261  dvres2lem  19262  dvres3  19265  dvcnp  19270  dvcnp2  19271  dvcn  19272  dvnff  19274  dvn2bss  19281  dvnres  19282  cpnord  19286  dvaddbr  19289  dvmulbr  19290  dvaddf  19293  dvmulf  19294  dvcobr  19297  dvcof  19299  dvnfre  19303  dvmptres2  19313  dvmptntr  19322  dvcnvlem  19325  dvcnv  19326  dvferm1lem  19333  dvferm2lem  19335  dvlip  19342  dvlipcn  19343  dvlip2  19344  c1liplem1  19345  dvgt0lem1  19351  lhop1lem  19362  lhop  19365  dvcnvrelem1  19366  dvcnvrelem2  19367  dvcnvre  19368  dvfsumle  19370  dvfsumge  19371  dvfsumabs  19372  ftc1lem1  19384  ftc1lem2  19385  ftc1a  19386  ftc1lem4  19388  ftc2ditglem  19394  itgsubstlem  19397  ig1peu  19559  ig1pdvds  19564  taylfvallem1  19738  tayl0  19743  taylply2  19749  taylply  19750  dvtaylp  19751  dvntaylp  19752  dvntaylp0  19753  taylthlem1  19754  ulmdvlem1  19779  ulmdvlem3  19781  psercn  19804  pserdvlem2  19806  abelth  19819  xrlimcnp  20265  wilthlem2  20309  sqff1o  20422  chtublem  20452  pntlemq  20752  pntlemf  20756  ghsubgolem  21039  shintcli  21910  shub1  21963  mdslmd1lem1  22907  mdexchi  22917  chirredlem1  22972  mdsymlem5  22989  sumdmdii  22997  sumdmdlem2  23001  xrsupssd  23256  pnfneige0  23376  xrge0tsmsd  23384  sigaclci  23495  insiga  23500  sssigagen2  23509  erdszelem7  23730  erdszelem8  23731  erdsze2lem1  23736  conpcon  23768  cvmliftmolem1  23814  cvmlift2lem1  23835  cvmlift2lem9  23844  cvmlift2lem10  23845  cvmlift3lem6  23857  cvmlift3lem7  23858  rtrclreclem.min  24046  dftrpred3g  24238  nofulllem3  24360  ontgval  24872  efilcp  25563  iscnp4  25574  islimrs4  25593  comppfsc  26318  neibastop2lem  26320  fnemeet2  26327  fnejoin1  26328  sstotbnd2  26509  heiborlem1  26546  heiborlem8  26553  intidl  26665  elrfi  26780  ismrcd1  26784  istopclsd  26786  mrefg2  26793  aomclem2  27163  aomclem6  27167  hbtlem6  27344  hbt  27345  symggen  27422  stoweidlem34  27794  bnj906  29035  bnj1020  29068  bnj1137  29098  bnj1408  29139  bnj1452  29155  lsmsat  29271  lssats  29275  lpssat  29276  lssatle  29278  lssat  29279  lsatcvatlem  29312  paddss12  30081  paddasslem17  30098  pmodlem1  30108  pmod1i  30110  pmodl42N  30113  elpcliN  30155  pclfinN  30162  polcon3N  30179  polcon2N  30181  paddunN  30189  pclfinclN  30212  poml5N  30216  osumcllem1N  30218  osumcllem2N  30219  osumcllem3N  30220  pl42lem2N  30242  pl42lem4N  30244  cdlemn5pre  31463  dihord1  31481  dihord2a  31482  dihord2b  31483  dihord5b  31522  dochss  31628  dochdmj1  31653  djhsumss  31670  djhunssN  31672  dochexmidlem2  31724  lclkrslem1  31800  lclkrslem2  31801  lcfrlem2  31806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator