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

Theorem sylan9req 2519
Description: An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.)
Hypotheses
Ref Expression
sylan9req.1
sylan9req.2
Assertion
Ref Expression
sylan9req

Proof of Theorem sylan9req
StepHypRef Expression
1 sylan9req.1 . . 3
21eqcomd 2465 . 2
3 sylan9req.2 . 2
42, 3sylan9eq 2518 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395
This theorem is referenced by:  fndmu  5687  fodmrnu  5808  funcoeqres  5851  tz7.44-3  7093  dfac5lem4  8528  zdiv  10958  hashimarni  12497  ccatws1lenrev  12635  fprodss  13755  dvdsmulc  14011  smumullem  14142  mgmidmo  15886  reslmhm2b  17700  fclsfnflim  20528  ustuqtop1  20744  ulm2  22780  sineq0  22914  cxple2a  23080  sqff1o  23456  eedimeq  24201  grpoidinvlem4  25209  hlimuni  26156  dmdsl3  27234  atoml2i  27302  disjpreima  27445  sspreima  27485  xrge0npcan  27684  eqfnun  30212  cncfiooicc  31697  fourierdlem41  31930  fourierdlem71  31960  sineq0ALT  33737  ltrncnvnid  35851  cdleme20j  36044  cdleme42ke  36211  dia2dimlem13  36803  dvh4dimN  37174  mapdval4N  37359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449
  Copyright terms: Public domain W3C validator