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

Theorem sstrd 3189
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 3187 . 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 3152
This theorem is referenced by:  syl5ss  3190  syl6ss  3191  ssdif2d  3315  uniintsn  3899  tfisi  4649  funss  5273  fssxp  5400  knatar  5857  suppssfv  6074  suppssov1  6075  tposss  6235  omwordri  6570  oewordri  6590  oeeui  6600  oaabs2  6643  omopthlem1  6653  ecinxp  6734  sbthlem1  6971  dffi2  7176  hartogslem1  7257  cantnfcl  7368  cantnflt  7373  cantnfp1lem3  7382  cantnflem3  7393  cnfcom  7403  cnfcom3lem  7406  rankssb  7520  tskwe  7583  dfac12lem2  7770  dfac12lem3  7771  cfflb  7885  cfcof  7900  ssfin2  7946  hsmexlem4  8055  ttukeylem6  8141  ttukeylem7  8142  fpwwe2lem1  8253  fpwwe2lem8  8259  fpwwe2lem11  8262  fpwwe2lem12  8263  canthnumlem  8270  canthwelem  8272  canthwe  8273  canthp1lem2  8275  pwfseqlem5  8285  wunex2  8360  tsktrss  8383  inttsk  8396  uzwo3  10311  seqsplit  11079  seqf1olem2a  11084  seqz  11094  swrdval2  11453  sumss  12197  qshash  12285  incexc  12296  incexc2  12297  rpnnen2lem11  12503  vdwlem1  13028  ramub1lem1  13073  imasaddvallem  13431  imasvscaf  13441  mrerintcl  13499  ismred2  13505  mremre  13506  mrcuni  13523  mressmrcd  13529  submrc  13530  mrissmrid  13543  mreexexlem2d  13547  isacs2  13555  isacs1i  13559  invss  13663  ssctr  13702  funcres2b  13771  isacs3lem  14269  acsfiindd  14280  acsmapd  14281  acsmap2d  14282  tsrdir  14360  subsubm  14434  gsumwspan  14468  subsubg  14640  subgint  14641  cntzidss  14813  pgpssslw  14925  lsmless1x  14955  lsmless2x  14956  lsmless12  14972  subglsm  14982  gsumval3  15191  gsumzadd  15204  gsum2d  15223  dmdprdd  15237  dprdfeq0  15257  dprdspan  15262  dprdres  15263  dprdss  15264  dprdz  15265  subgdmdprd  15269  subgdprd  15270  dprdsn  15271  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  dprdsplit  15283  pgpfac1lem2  15310  pgpfac1lem3  15312  pgpfac1lem5  15314  subsubrg  15571  lspss  15741  lspun  15744  lsslsp  15772  lmhmlsp  15806  lsmelval2  15838  lsmssspx  15841  lsppratlem2  15901  lsppratlem3  15902  lsppratlem4  15903  lbsextlem2  15912  lbsextlem3  15913  aspss  16072  ocvlsp  16576  cssmre  16593  obselocv  16628  obslbs  16630  toponmre  16830  neiint  16841  neiss  16846  lpss  16874  lpss3  16876  restopnb  16906  restfpw  16910  restcls  16911  restntr  16912  restlp  16913  ordtbas  16922  pnfnei  16950  mnfnei  16951  cnclsi  17001  isreg2  17105  discmp  17125  cmpcld  17129  uncmp  17130  sscmp  17132  hauscmplem  17133  cmpfi  17135  iunconlem  17153  clscon  17156  2ndcctbss  17181  restnlly  17208  llyrest  17211  nllyrest  17212  llyidm  17214  nllyidm  17215  cldllycmp  17221  dislly  17223  llycmpkgen2  17245  ptbasfi  17276  txnlly  17331  txcmplem1  17335  tx1stc  17344  xkococnlem  17353  qtopval2  17387  basqtop  17402  tgqtop  17403  qtoprest  17408  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  fsubbas  17562  fgabs  17574  fbasrn  17579  trfil2  17582  trfg  17586  isufil2  17603  trufil  17605  ssufl  17613  ufileu  17614  filufint  17615  fmfnfmlem4  17652  fmfnfm  17653  flimss2  17667  flimss1  17668  fclsfnflim  17722  flimfnfcls  17723  fclscmp  17725  cnpfcfi  17735  alexsubALT  17745  clssubg  17791  clsnsg  17792  blss  17972  blcld  18051  blsscls  18053  met1stc  18067  met2ndci  18068  tgqioo  18306  xrsblre  18317  reconnlem2  18332  xrge0gsumle  18338  xrge0tsms  18339  rescncf  18401  cnmpt2pc  18426  cnheibor  18453  cnllycmp  18454  lebnum  18462  phtpycn  18481  cfilfcls  18700  iscmet3lem2  18718  cmetss  18740  cncmet  18744  bcthlem4  18749  bcth3  18753  minveclem4a  18794  minveclem4  18796  ivthicc  18818  ovollb  18838  ovollb2lem  18847  ovollb2  18848  nulmbl2  18894  ioorcl2  18927  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  opnmbllem  18956  volcn  18961  volivth  18962  mbfeqalem  18997  itg10a  19065  mbfi1fseqlem4  19073  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  limcflf  19231  limcres  19236  dvbss  19251  dvbsss  19252  perfdvf  19253  dvreslem  19259  dvres2lem  19260  dvres3  19263  dvcnp  19268  dvcnp2  19269  dvcn  19270  dvnff  19272  dvn2bss  19279  dvnres  19280  cpnord  19284  dvaddbr  19287  dvmulbr  19288  dvaddf  19291  dvmulf  19292  dvcobr  19295  dvcof  19297  dvnfre  19301  dvmptres2  19311  dvmptntr  19320  dvcnvlem  19323  dvcnv  19324  dvferm1lem  19331  dvferm2lem  19333  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  dvgt0lem1  19349  lhop1lem  19360  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcnvre  19366  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  ftc1lem1  19382  ftc1lem2  19383  ftc1a  19384  ftc1lem4  19386  ftc2ditglem  19392  itgsubstlem  19395  ig1peu  19557  ig1pdvds  19562  taylfvallem1  19736  tayl0  19741  taylply2  19747  taylply  19748  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  ulmdvlem1  19777  ulmdvlem3  19779  psercn  19802  pserdvlem2  19804  abelth  19817  xrlimcnp  20263  wilthlem2  20307  sqff1o  20420  chtublem  20450  pntlemq  20750  pntlemf  20754  ghsubgolem  21037  shintcli  21908  shub1  21961  mdslmd1lem1  22905  mdexchi  22915  chirredlem1  22970  mdsymlem5  22987  sumdmdii  22995  sumdmdlem2  22999  xrsupssd  23254  pnfneige0  23374  xrge0tsmsd  23382  sigaclci  23493  insiga  23498  sssigagen2  23507  erdszelem7  23728  erdszelem8  23729  erdsze2lem1  23734  conpcon  23766  cvmliftmolem1  23812  cvmlift2lem1  23833  cvmlift2lem9  23842  cvmlift2lem10  23843  cvmlift3lem6  23855  cvmlift3lem7  23856  rtrclreclem.min  24044  dftrpred3g  24236  nofulllem3  24358  ontgval  24870  efilcp  25552  iscnp4  25563  islimrs4  25582  comppfsc  26307  neibastop2lem  26309  fnemeet2  26316  fnejoin1  26317  sstotbnd2  26498  heiborlem1  26535  heiborlem8  26542  intidl  26654  elrfi  26769  ismrcd1  26773  istopclsd  26775  mrefg2  26782  aomclem2  27152  aomclem6  27156  hbtlem6  27333  hbt  27334  symggen  27411  stoweidlem34  27783  bnj906  28962  bnj1020  28995  bnj1137  29025  bnj1408  29066  bnj1452  29082  lsmsat  29198  lssats  29202  lpssat  29203  lssatle  29205  lssat  29206  lsatcvatlem  29239  paddss12  30008  paddasslem17  30025  pmodlem1  30035  pmod1i  30037  pmodl42N  30040  elpcliN  30082  pclfinN  30089  polcon3N  30106  polcon2N  30108  paddunN  30116  pclfinclN  30139  poml5N  30143  osumcllem1N  30145  osumcllem2N  30146  osumcllem3N  30147  pl42lem2N  30169  pl42lem4N  30171  cdlemn5pre  31390  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord5b  31449  dochss  31555  dochdmj1  31580  djhsumss  31597  djhunssN  31599  dochexmidlem2  31651  lclkrslem1  31727  lclkrslem2  31728  lcfrlem2  31733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator