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

Theorem syl6sseqr 3644
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 2629 . 2 𝐵 = 𝐶
41, 3syl6sseq 3643 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  disjxiun  4640  disjxiunOLD  4641  knatar  6592  iunpw  6963  wfrdmcl  7408  wfrlem12  7411  wfrlem16  7415  wfrlem17  7416  tfrlem9  7466  tfrlem9a  7467  tfrlem13  7471  tz7.44-2  7488  tz7.44-3  7489  tz7.49  7525  marypha1lem  8324  ordtypelem2  8409  ixpiunwdom  8481  oemapvali  8566  tcss  8605  tcel  8606  pwwf  8655  rankpwi  8671  rankval3b  8674  cplem1  8737  dfac12lem2  8951  infmap2  9025  ackbij1b  9046  ttukeylem6  9321  fpwwe2lem11  9447  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwe2  9450  uznnssnn  11720  shftfval  13791  rexuzre  14073  climsup  14381  clim2prod  14601  fprodntriv  14653  eulerthlem2  15468  ramtlecl  15685  mreexexlem4d  16288  mreexdomd  16291  gsumpropd2lem  17254  gsumzaddlem  18302  gsum2d  18352  telgsums  18371  pgpfac1lem1  18454  pgpfac1lem3a  18456  pgpfac1lem3  18457  pgpfac1lem5  18459  lspsolvlem  19123  lbsextlem2  19140  dsmmacl  20066  eltopss  20693  difopn  20819  tgrest  20944  perfopn  20970  pnfnei  21005  mnfnei  21006  regsep2  21161  cncmp  21176  uncmp  21187  hauscmplem  21190  hauscmp  21191  conndisj  21200  cnconn  21206  conncompss  21217  2ndcctbss  21239  islly2  21268  comppfsc  21316  1stckgenlem  21337  txuni2  21349  ptbasfi  21365  ptpjopn  21396  txindis  21418  txtube  21424  hausdiag  21429  xkoinjcn  21471  tgqtop  21496  filconn  21668  elfm2  21733  flimclslem  21769  flffbas  21780  fclsbas  21806  flimfnfcls  21813  alexsubALT  21836  symgtgp  21886  ustssco  21999  isucn2  22064  ucnima  22066  ucnprima  22067  blcls  22292  prdsxmslem2  22315  isngp2  22382  tgioo  22580  xrtgioo  22590  xrsmopn  22596  opnreen  22615  cnheiborlem  22734  cnllycmp  22736  tchcph  23017  rrxmvallem  23168  uniioombllem4  23335  dyadmbllem  23348  opnmbllem  23350  mbfimaopnlem  23403  mbflimsup  23414  i1fadd  23443  i1fmul  23444  itg1addlem4  23447  i1fmulc  23451  limciun  23639  dvlip2  23739  c1lip3  23743  lhop  23760  dvfsumlem2  23771  dvfsumrlimge0  23774  dvfsumrlim2  23776  ulmval  24115  psercnlem2  24159  efopnlem2  24384  efopn  24385  umgrres1lem  26183  upgrres1  26186  nbgrssvwo2  26242  ubthlem1  27696  issh2  28036  mdsymlem1  29232  padct  29471  xrofsup  29507  fz2ssnn0  29521  tpr2rico  29932  sibfinima  30375  fct2relem  30649  bnj906  30974  bnj1014  31004  bnj1286  31061  bnj1408  31078  bnj1450  31092  bnj1452  31094  bnj1498  31103  bnj1501  31109  cvmopnlem  31234  cvmfolem  31235  cvmliftlem6  31246  cvmliftlem8  31248  cvmliftlem13  31252  cvmliftlem15  31254  cvmlift2lem9  31267  cvmlift2lem11  31269  cvmlift2lem12  31270  mclsppslem  31454  trpredpred  31702  trpredtr  31704  trpredrec  31712  frrlem5e  31762  frrlem11  31766  filnetlem4  32351  dissneqlem  33158  lindsdom  33374  opnmbllem0  33416  cnambfre  33429  heibor1lem  33579  osumcllem1N  35061  osumcllem2N  35062  pexmidlem6N  35080  dochexmidlem6  36573  dochexmidlem7  36574  mapdrvallem3  36754  k0004ss2  38270  dvsconst  38349  dvsid  38350  dvsef  38351  iunconnlem2  38991  uzssd2  39457  climinf  39638  climsuse  39640  climresmpt  39691  climleltrp  39708  stoweidlem28  40008  stoweidlem50  40030  stoweidlem52  40032  stoweidlem53  40033  stoweidlem54  40034  fourierdlem54  40140  fourierdlem80  40166  meaiininclem  40463  caratheodorylem2  40504  hspmbllem2  40604  mbfresmf  40711  smfmbfcex  40731  smflimlem2  40743  smflimsuplem2  40790  smflimsuplem3  40791  smflimsuplem5  40793  smflimsuplem6  40794  pfxccatpfx2  41193  upgredgssspr  41516  setrec1  42203  aacllem  42312
  Copyright terms: Public domain W3C validator