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

Theorem syl6sseqr 3614
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl6ssr.1 (𝜑𝐴𝐵)
syl6ssr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6sseqr (𝜑𝐴𝐶)

Proof of Theorem syl6sseqr
StepHypRef Expression
1 syl6ssr.1 . 2 (𝜑𝐴𝐵)
2 syl6ssr.2 . . 3 𝐶 = 𝐵
32eqcomi 2618 . 2 𝐵 = 𝐶
41, 3syl6sseq 3613 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  disjxiun  4573  disjxiunOLD  4574  knatar  6485  iunpw  6847  wfrdmcl  7287  wfrlem12  7290  wfrlem16  7294  wfrlem17  7295  tfrlem9  7345  tfrlem9a  7346  tfrlem13  7350  tz7.44-2  7367  tz7.44-3  7368  tz7.49  7404  marypha1lem  8199  ordtypelem2  8284  ixpiunwdom  8356  oemapvali  8441  tcss  8480  tcel  8481  pwwf  8530  rankpwi  8546  rankval3b  8549  cplem1  8612  dfac12lem2  8826  infmap2  8900  ackbij1b  8921  ttukeylem6  9196  fpwwe2lem11  9318  fpwwe2lem12  9319  fpwwe2lem13  9320  fpwwe2  9321  uznnssnn  11567  shftfval  13604  rexuzre  13886  climsup  14194  clim2prod  14405  fprodntriv  14457  eulerthlem2  15271  ramtlecl  15488  mreexexlem4d  16076  mreexdomd  16079  gsumpropd2lem  17042  gsumzaddlem  18090  gsum2d  18140  telgsums  18159  pgpfac1lem1  18242  pgpfac1lem3a  18244  pgpfac1lem3  18245  pgpfac1lem5  18247  lspsolvlem  18909  lbsextlem2  18926  dsmmacl  19846  eltopss  20479  difopn  20590  tgrest  20715  perfopn  20741  pnfnei  20776  mnfnei  20777  regsep2  20932  cncmp  20947  uncmp  20958  hauscmplem  20961  hauscmp  20962  conndisj  20971  cnconn  20977  concompss  20988  2ndcctbss  21010  islly2  21039  comppfsc  21087  1stckgenlem  21108  txuni2  21120  ptbasfi  21136  ptpjopn  21167  txindis  21189  txtube  21195  hausdiag  21200  xkoinjcn  21242  tgqtop  21267  filcon  21439  elfm2  21504  flimclslem  21540  flffbas  21551  fclsbas  21577  flimfnfcls  21584  alexsubALT  21607  symgtgp  21657  ustssco  21770  isucn2  21835  ucnima  21837  ucnprima  21838  blcls  22062  prdsxmslem2  22085  isngp2  22152  tgioo  22339  xrtgioo  22349  xrsmopn  22355  opnreen  22374  cnheiborlem  22492  cnllycmp  22494  tchcph  22765  rrxmvallem  22912  uniioombllem4  23077  dyadmbllem  23090  opnmbllem  23092  mbfimaopnlem  23145  mbflimsup  23156  i1fadd  23185  i1fmul  23186  itg1addlem4  23189  i1fmulc  23193  limciun  23381  dvlip2  23479  c1lip3  23483  lhop  23500  dvfsumlem2  23511  dvfsumrlimge0  23514  dvfsumrlim2  23516  ulmval  23855  psercnlem2  23899  efopnlem2  24120  efopn  24121  nbgrassvwo2  25733  ubthlem1  26916  issh2  27256  mdsymlem1  28452  padct  28691  xrofsup  28729  tpr2rico  29092  sibfinima  29534  bnj906  30060  bnj1014  30090  bnj1286  30147  bnj1408  30164  bnj1450  30178  bnj1452  30180  bnj1498  30189  bnj1501  30195  cvmopnlem  30320  cvmfolem  30321  cvmliftlem6  30332  cvmliftlem8  30334  cvmliftlem13  30338  cvmliftlem15  30340  cvmlift2lem9  30353  cvmlift2lem11  30355  cvmlift2lem12  30356  mclsppslem  30540  trpredpred  30778  trpredtr  30780  trpredrec  30788  frrlem5e  30838  frrlem11  30842  filnetlem4  31352  dissneqlem  32166  lindsdom  32376  opnmbllem0  32418  cnambfre  32431  heibor1lem  32581  osumcllem1N  34063  osumcllem2N  34064  pexmidlem6N  34082  dochexmidlem6  35575  dochexmidlem7  35576  mapdrvallem3  35756  k0004ss2  37273  dvsconst  37354  dvsid  37355  dvsef  37356  iunconlem2  37996  climinf  38477  climsuse  38479  climresmpt  38530  climleltrp  38547  stoweidlem28  38725  stoweidlem50  38747  stoweidlem52  38749  stoweidlem53  38750  stoweidlem54  38751  fourierdlem54  38857  fourierdlem80  38883  meaiininclem  39180  caratheodorylem2  39221  hspmbllem2  39321  mbfresmf  39430  smfmbfcex  39450  smflimlem2  39462  pfxccatpfx2  40096  umgrres1lem  40531  upgrres1  40534  nbgrssvwo2  40589  aacllem  42319
  Copyright terms: Public domain W3C validator