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

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

Proof of Theorem syl6sseq
StepHypRef Expression
1 syl6sseq.1 . 2  |-  ( ph  ->  A  C_  B )
2 syl6sseq.2 . . 3  |-  B  =  C
32sseq2i 3425 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3sylib 201 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1448    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386
This theorem is referenced by:  syl6sseqr  3447  sofld  5262  relrelss  5338  foimacnv  5814  onfununi  7047  hartogslem1  8044  cantnfp1lem3  8172  uniwf  8277  rankeq0b  8318  cflecard  8670  fin23lem16  8752  fin23lem41  8769  pwcfsdom  8995  fpwwe2lem13  9054  fpwwe2  9055  canth4  9059  hashbclem  12610  dmtrclfv  13093  zsum  13795  fsumcvg3  13806  incexclem  13905  zprod  14002  ramub1lem1  14995  imasaddfnlem  15445  imasvscafn  15454  mremre  15521  submre  15522  mreexexlem3d  15563  isacs1i  15574  acsmapd  16435  acsmap2d  16436  gsumzoppg  17588  lspsntri  18331  lsppratlem4  18384  lbsextlem3  18394  distop  20022  elcls  20100  cnpresti  20315  cnprest  20316  cmpcld  20428  cnconn  20448  iuncon  20454  comppfsc  20558  ptuni2  20602  alexsubALTlem3  21075  ustssco  21240  ust0  21245  ustbas2  21251  ustimasn  21254  utopbas  21261  utop2nei  21276  setsmstopn  21504  metustsym  21581  metust  21584  tngtopn  21669  ovoliunlem1  22466  lhop1lem  22977  ig1peu  23134  ig1peuOLD  23135  ig1pdvds  23140  ig1pdvdsOLD  23146  logccv  23620  amgmlem  23927  shsupcl  27003  shsupunss  27011  shslubi  27050  orthin  27111  h1datomi  27246  mdslj2i  27985  mdslmd1lem1  27990  pwuniss  28178  iundifdifd  28187  difres  28220  fresf1o  28240  metideq  28703  hauseqcn  28708  tpr2rico  28725  esumrnmpt2  28896  esumpfinvallem  28902  esum2d  28921  omssubadd  29134  omssubaddOLD  29138  carsggect  29156  omsmeas  29161  omsmeasOLD  29162  orvcelval  29307  signsply0  29446  cvmlift2lem11  30042  cvmlift2lem12  30043  dfon2lem7  30441  filnetlem3  31042  onsucsuccmpi  31109  dissneqlem  31744  icoreunrn  31764  mblfinlem1  31979  ismblfin  31983  sstotbnd2  32108  dochexmidlem4  35033  lcfrlem38  35150  ismrcd1  35542  eldioph2lem2  35605  rmxyelqirr  35760  hbt  35991  rngunsnply  36041  iocinico  36098  dmtrcl  36236  rntrcl  36237  trrelsuperrel2dg  36265  unirnmapsn  37508  limciccioolb  37743  limcrecl  37751  limcicciooub  37759  stoweidlem50  37968  stoweidlem52  37970  stoweidlem53  37971  stoweidlem57  37975  stoweidlem59  37977  fourierdlem50  38077  fourierdlem103  38130  fourierdlem104  38131  pwsal  38233  sge0iun  38320  sge0isum  38328  meadjuni  38356  omessle  38383  upgr1e  39301  uspgr1e  39421  zlmodzxzel  40461  lincresunit3  40599
  Copyright terms: Public domain W3C validator