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

Theorem sstrd 3190
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 3188 . 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 3153
This theorem is referenced by:  syl5ss  3191  syl6ss  3192  ssdif2d  3316  uniintsn  3900  tfisi  4648  funss  5239  fssxp  5366  knatar  5819  suppssfv  6036  suppssov1  6037  tposss  6197  omwordri  6566  oewordri  6586  oeeui  6596  oaabs2  6639  omopthlem1  6649  ecinxp  6730  sbthlem1  6967  dffi2  7172  hartogslem1  7253  cantnfcl  7364  cantnflt  7369  cantnfp1lem3  7378  cantnflem3  7389  cnfcom  7399  cnfcom3lem  7402  rankssb  7516  tskwe  7579  dfac12lem2  7766  dfac12lem3  7767  cfflb  7881  cfcof  7896  ssfin2  7942  hsmexlem4  8051  ttukeylem6  8137  ttukeylem7  8138  fpwwe2lem1  8249  fpwwe2lem8  8255  fpwwe2lem11  8258  fpwwe2lem12  8259  canthnumlem  8266  canthwelem  8268  canthwe  8269  canthp1lem2  8271  pwfseqlem5  8281  wunex2  8356  tsktrss  8379  inttsk  8392  uzwo3  10307  seqsplit  11075  seqf1olem2a  11080  seqz  11090  swrdval2  11449  sumss  12193  qshash  12281  incexc  12292  incexc2  12293  rpnnen2lem11  12499  vdwlem1  13024  ramub1lem1  13069  imasaddvallem  13427  imasvscaf  13437  mrerintcl  13495  ismred2  13501  mremre  13502  mrcuni  13519  mressmrcd  13525  submrc  13526  mrissmrid  13539  mreexexlem2d  13543  isacs2  13551  isacs1i  13555  invss  13659  ssctr  13698  funcres2b  13767  isacs3lem  14265  acsfiindd  14276  acsmapd  14277  acsmap2d  14278  tsrdir  14356  subsubm  14430  gsumwspan  14464  subsubg  14636  subgint  14637  cntzidss  14809  pgpssslw  14921  lsmless1x  14951  lsmless2x  14952  lsmless12  14968  subglsm  14978  gsumval3  15187  gsumzadd  15200  gsum2d  15219  dmdprdd  15233  dprdfeq0  15253  dprdspan  15258  dprdres  15259  dprdss  15260  dprdz  15261  subgdmdprd  15265  subgdprd  15266  dprdsn  15267  dprd2dlem1  15272  dprd2da  15273  dmdprdsplit2lem  15276  dprdsplit  15279  pgpfac1lem2  15306  pgpfac1lem3  15308  pgpfac1lem5  15310  subsubrg  15567  lspss  15737  lspun  15740  lsslsp  15768  lmhmlsp  15802  lsmelval2  15834  lsmssspx  15837  lsppratlem2  15897  lsppratlem3  15898  lsppratlem4  15899  lbsextlem2  15908  lbsextlem3  15909  aspss  16068  ocvlsp  16572  cssmre  16589  obselocv  16624  obslbs  16626  toponmre  16826  neiint  16837  neiss  16842  lpss  16870  lpss3  16872  restopnb  16902  restfpw  16906  restcls  16907  restntr  16908  restlp  16909  ordtbas  16918  pnfnei  16946  mnfnei  16947  cnclsi  16997  isreg2  17101  discmp  17121  cmpcld  17125  uncmp  17126  sscmp  17128  hauscmplem  17129  cmpfi  17131  iunconlem  17149  clscon  17152  2ndcctbss  17177  restnlly  17204  llyrest  17207  nllyrest  17208  llyidm  17210  nllyidm  17211  cldllycmp  17217  dislly  17219  llycmpkgen2  17241  ptbasfi  17272  txnlly  17327  txcmplem1  17331  tx1stc  17340  xkococnlem  17349  qtopval2  17383  basqtop  17398  tgqtop  17399  qtoprest  17404  kqreglem1  17428  kqreglem2  17429  kqnrmlem1  17430  kqnrmlem2  17431  fsubbas  17558  fgabs  17570  fbasrn  17575  trfil2  17578  trfg  17582  isufil2  17599  trufil  17601  ssufl  17609  ufileu  17610  filufint  17611  fmfnfmlem4  17648  fmfnfm  17649  flimss2  17663  flimss1  17664  fclsfnflim  17718  flimfnfcls  17719  fclscmp  17721  cnpfcfi  17731  alexsubALT  17741  clssubg  17787  clsnsg  17788  blss  17968  blcld  18047  blsscls  18049  met1stc  18063  met2ndci  18064  tgqioo  18302  xrsblre  18313  reconnlem2  18328  xrge0gsumle  18334  xrge0tsms  18335  rescncf  18397  cnmpt2pc  18422  cnheibor  18449  cnllycmp  18450  lebnum  18458  phtpycn  18477  cfilfcls  18696  iscmet3lem2  18714  cmetss  18736  cncmet  18740  bcthlem4  18745  bcth3  18749  minveclem4a  18790  minveclem4  18792  ivthicc  18814  ovollb  18834  ovollb2lem  18843  ovollb2  18844  nulmbl2  18890  ioorcl2  18923  uniioombllem3  18936  uniioombllem4  18937  uniioombllem5  18938  opnmbllem  18952  volcn  18957  volivth  18958  mbfeqalem  18993  itg10a  19061  mbfi1fseqlem4  19069  ditgcl  19204  ditgswap  19205  ditgsplitlem  19206  limcflf  19227  limcres  19232  dvbss  19247  dvbsss  19248  perfdvf  19249  dvreslem  19255  dvres2lem  19256  dvres3  19259  dvcnp  19264  dvcnp2  19265  dvcn  19266  dvnff  19268  dvn2bss  19275  dvnres  19276  cpnord  19280  dvaddbr  19283  dvmulbr  19284  dvaddf  19287  dvmulf  19288  dvcobr  19291  dvcof  19293  dvnfre  19297  dvmptres2  19307  dvmptntr  19316  dvcnvlem  19319  dvcnv  19320  dvferm1lem  19327  dvferm2lem  19329  dvlip  19336  dvlipcn  19337  dvlip2  19338  c1liplem1  19339  dvgt0lem1  19345  lhop1lem  19356  lhop  19359  dvcnvrelem1  19360  dvcnvrelem2  19361  dvcnvre  19362  dvfsumle  19364  dvfsumge  19365  dvfsumabs  19366  ftc1lem1  19378  ftc1lem2  19379  ftc1a  19380  ftc1lem4  19382  ftc2ditglem  19388  itgsubstlem  19391  ig1peu  19553  ig1pdvds  19558  taylfvallem1  19732  tayl0  19737  taylply2  19743  taylply  19744  dvtaylp  19745  dvntaylp  19746  dvntaylp0  19747  taylthlem1  19748  ulmdvlem1  19773  ulmdvlem3  19775  psercn  19798  pserdvlem2  19800  abelth  19813  xrlimcnp  20259  wilthlem2  20303  sqff1o  20416  chtublem  20446  pntlemq  20746  pntlemf  20750  ghsubgolem  21031  shintcli  21904  shub1  21957  mdslmd1lem1  22901  mdexchi  22911  chirredlem1  22966  mdsymlem5  22983  sumdmdii  22991  sumdmdlem2  22995  erdszelem7  23135  erdszelem8  23136  erdsze2lem1  23141  conpcon  23173  cvmliftmolem1  23219  cvmlift2lem1  23240  cvmlift2lem9  23249  cvmlift2lem10  23250  cvmlift3lem6  23262  cvmlift3lem7  23263  rtrclreclem.min  23451  dftrpred3g  23640  ontgval  24280  efilcp  24963  iscnp4  24974  islimrs4  24993  comppfsc  25718  neibastop2lem  25720  fnemeet2  25727  fnejoin1  25728  sstotbnd2  25909  heiborlem1  25946  heiborlem8  25953  intidl  26065  elrfi  26180  ismrcd1  26184  istopclsd  26186  mrefg2  26193  aomclem2  26563  aomclem6  26567  hbtlem6  26744  hbt  26745  symggen  26822  stoweidlem34  27194  bnj906  28241  bnj1020  28274  bnj1137  28304  bnj1408  28345  bnj1452  28361  lsmsat  28477  lssats  28481  lpssat  28482  lssatle  28484  lssat  28485  lsatcvatlem  28518  paddss12  29287  paddasslem17  29304  pmodlem1  29314  pmod1i  29316  pmodl42N  29319  elpcliN  29361  pclfinN  29368  polcon3N  29385  polcon2N  29387  paddunN  29395  pclfinclN  29418  poml5N  29422  osumcllem1N  29424  osumcllem2N  29425  osumcllem3N  29426  pl42lem2N  29448  pl42lem4N  29450  cdlemn5pre  30669  dihord1  30687  dihord2a  30688  dihord2b  30689  dihord5b  30728  dochss  30834  dochdmj1  30859  djhsumss  30876  djhunssN  30878  dochexmidlem2  30930  lclkrslem1  31006  lclkrslem2  31007  lcfrlem2  31012
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator