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

Theorem syl5eqss 3222
Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqss.1  |-  A  =  B
syl5eqss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5eqss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5eqss
StepHypRef Expression
1 syl5eqss.2 . 2  |-  ( ph  ->  B  C_  C )
2 syl5eqss.1 . . 3  |-  A  =  B
32sseq1i 3202 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3sylibr 203 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  syl5eqssr  3223  inss  3398  fr3nr  4571  suceloni  4604  xpsspw  4797  xpsspwOLD  4798  fun  5405  fun11iun  5493  fmpt  5681  fliftrel  5807  knatar  5857  suppss2  6073  1stcof  6147  2ndcof  6148  fnwelem  6230  oeeui  6600  cantnfp1lem1  7380  cantnfp1lem3  7382  cantnflem1d  7390  cantnflem1  7391  aceq3lem  7747  cflecard  7879  cfslb2n  7894  itunitc1  8046  axdc3lem2  8077  fpwwe2lem12  8263  canthwelem  8272  wuncval2  8369  gruiun  8421  peano5nni  9749  un0addcl  9997  un0mulcl  9998  mertenslem2  12341  4sqlem11  13002  4sqlem19  13010  vdwlem13  13040  imasless  13442  rescfth  13811  oppchofcl  14034  oyoncl  14044  gsumvallem1  14448  efgsfo  15048  efgcpbllemb  15064  frgpuplem  15081  gsumzaddlem  15203  dprdfid  15252  dprd2d2  15279  ablfacrp  15301  ablfac1b  15305  ablfac1eu  15308  pgpfac1lem5  15314  ablfaclem3  15322  lsptpcl  15736  lsppratlem3  15902  lsppratlem4  15903  lbsextlem2  15912  topsn  16673  ordtbaslem  16918  ordtuni  16920  ordtbas2  16921  cnpco  16996  cnconst2  17011  tgcmp  17128  iuncon  17154  ptuni2  17271  xkococnlem  17353  tgqtop  17403  fbasrn  17579  uzrest  17592  fmco  17656  alexsubALT  17745  snclseqg  17798  imasdsf1olem  17937  xmetresbl  17983  blsscls2  18050  tngtopn  18166  reconn  18333  metnrmlem3  18365  cphsubrglem  18613  minveclem1  18788  minveclem3b  18792  ovolficcss  18829  ovolicc2lem4  18879  iundisj2  18906  uniioombllem4  18941  vitalilem5  18967  mbfeqalem  18997  itg1addlem4  19054  limciun  19244  dvlip2  19342  dv11cn  19348  aalioulem3  19714  pserdvlem2  19804  pserdv  19805  abelthlem2  19808  efif1o  19908  efrlim  20264  fsumdvdsmul  20435  perfectlem2  20469  minvecolem1  21453  sh0le  22019  mdslmd3i  22912  suppss2f  23201  iundisj2fi  23364  iundisj2f  23366  blscon  23775  cvmliftlem2  23817  cvmlift2lem12  23845  eupares  23899  ghomfo  23998  relexpdm  24032  relexprn  24033  trpredss  24232  trpredmintr  24234  frrlem5d  24288  areacirclem4  24927  trunitr  25109  cmptdst  25568  limptlimpr2lem1  25574  prismorcsetlemc  25917  neibastop2lem  26309  filnetlem3  26329  sdclem1  26453  istotbnd3  26495  sstotbnd  26499  iccbnd  26564  icccmpALT  26565  f1lindf  27292  hbtlem6  27333  stoweidlem14  27763  bnj849  28957  bnj1136  29027  bnj1311  29054  bnj1413  29065  bnj1452  29082  osumcllem1N  30145  osumcllem2N  30146  osumcllem4N  30148  osumcllem9N  30153  pexmidlem6N  30164  dihglblem3N  31485  dvhdimlem  31634  dochexmidlem6  31655  lcfrlem16  31748  lcfr  31775
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