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

Theorem syl5req 2481
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5req.1  |-  A  =  B
syl5req.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
syl5req  |-  ( ph  ->  C  =  A )

Proof of Theorem syl5req
StepHypRef Expression
1 syl5req.1 . . 3  |-  A  =  B
2 syl5req.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2syl5eq 2480 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2441 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  syl5reqr  2483  opeqsn  4452  ordintdif  4630  relop  5023  funopg  5485  funcnvres  5522  nneob  6895  sucdom2  7303  unblem2  7360  pwfilem  7401  kmlem2  8031  kmlem11  8040  kmlem12  8041  cflim3  8142  1idsr  8973  recextlem1  9652  nn0supp  10273  quoremz  11236  quoremnn0ALT  11238  intfrac2  11239  hashprg  11666  hashfacen  11703  leiso  11708  cvgcmpce  12597  explecnv  12644  ramub1lem1  13394  ressress  13526  subsubc  14050  efginvrel2  15359  efgredleme  15375  efgcpbllemb  15387  frgpnabllem1  15484  gsumzmhm  15533  dprd2da  15600  dpjcntz  15610  dpjdisj  15611  dpjlsm  15612  dpjidcl  15616  ablfac1lem  15626  ablfac1eu  15631  lmhmlsp  16125  mplmon2mul  16561  neitr  17244  fixufil  17954  trust  18259  restmetu  18617  nmfval2  18638  nmval2  18639  rerest  18835  xrrest  18838  xrge0gsumle  18864  voliunlem3  19446  volsup  19450  itg1addlem5  19592  itg2monolem1  19642  itg2cnlem2  19654  itgmpt  19674  iblcnlem1  19679  itgcnlem  19681  itgioo  19707  limcres  19773  mdegfval  19985  dgrlem  20148  coeidlem  20156  mcubic  20687  binom4  20690  dquartlem2  20692  amgm  20829  wilthlem2  20852  rpvmasum2  21206  pntlemo  21301  wlkntrllem3  21561  opidon2  21912  vc2  22034  nvge0  22163  nmoo0  22292  bcsiALT  22681  pjchi  22934  shjshseli  22995  spanpr  23082  pjinvari  23694  mdslmd1lem2  23829  iundifdifd  24012  iundifdif  24013  gtiso  24088  esumpr2  24458  lgamgulmlem2  24814  eflgam  24829  risefallfac  25340  dvreasin  26290  topjoin  26394  tailfval  26401  tailf  26404  elrfi  26748  fzsplit1nn0  26812  rabdiophlem2  26862  eldioph4b  26872  diophren  26874  pell1qrgaplem  26936  rngunsnply  27355  psgnunilem1  27393  compne  27619  fmuldfeq  27689  stoweidlem44  27769  swrdccat3a  28217  frgrancvvdeqlem4  28422  cdleme4  31035  cdleme22e  31141  cdleme22eALTN  31142  cdleme42a  31268  cdleme42d  31270  cdlemk20  31671  dih1dimatlem0  32126  lcfrlem2  32341
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator