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

Theorem syl5req 2469
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 2468 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2428 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-cleq 2415
This theorem is referenced by:  syl5reqr  2471  opeqsn  4652  relop  4940  ordintdif  5427  funopg  5569  funcnvres  5606  csbriota  6216  csbov123  6276  mpt2curryd  6964  nneob  7301  sucdom2  7714  unblem2  7770  pwfilem  7814  kmlem2  8525  kmlem11  8534  kmlem12  8535  cflim3  8636  1idsr  9466  recextlem1  10186  quoremz  12025  quoremnn0ALT  12027  intfrac2  12028  hashprg  12515  hashfacen  12558  leiso  12563  ccatrid  12672  swrdccat3a  12789  repsw2  12962  repsw3  12963  cvgcmpce  13814  explecnv  13859  risefallfac  14013  ramub1lem1  14920  ressress  15123  subsubc  15694  psgnunilem1  17070  psgn0fv0  17088  psgnsn  17097  efginvrel2  17313  efgredleme  17329  efgcpbllemb  17341  frgpnabllem1  17445  gsumzaddlem  17490  gsumzmhm  17506  fsfnn0gsumfsffz  17548  dprd2da  17611  dpjcntz  17621  dpjdisj  17622  dpjlsm  17623  dpjidcl  17627  ablfac1lem  17637  ablfac1eu  17642  lmhmlsp  18208  mplmon2mul  18660  frlmip  19271  1marepvmarrepid  19535  m1detdiag  19557  cramerimplem2  19644  pmatcollpw3lem  19742  chpscmatgsumbin  19803  chpscmatgsummon  19804  cayhamlem2  19843  neitr  20131  fixufil  20872  trust  21179  restmetu  21520  nmfval2  21540  nmval2  21541  rerest  21757  xrrest  21760  xrge0gsumle  21786  rrxip  22284  voliunlem3  22440  volsup  22444  itg1addlem5  22593  itg2monolem1  22643  itg2cnlem2  22655  itgmpt  22675  iblcnlem1  22680  itgcnlem  22682  itgioo  22708  limcres  22776  mdegfval  22946  dgrlem  23118  coeidlem  23126  mcubic  23708  binom4  23711  dquartlem2  23713  amgm  23851  lgamgulmlem2  23890  eflgam  23905  wilthlem2  23929  rpvmasum2  24285  pntlemo  24380  wlkntrllem3  25226  frgrancvvdeqlem4  25696  opidon2OLD  25987  vc2  26109  nvge0  26238  nmoo0  26367  bcsiALT  26767  pjchi  27020  shjshseli  27081  spanpr  27168  pjinvari  27779  mdslmd1lem2  27914  iundifdifd  28116  iundifdif  28117  gtiso  28220  rngurd  28496  esumpr2  28833  omssubaddlem  29072  eulerpartlemt  29149  ofcccat  29375  topjoin  30963  tailfval  30970  tailf  30973  dvasin  31929  dvacos  31930  cdleme4  33710  cdleme22e  33817  cdleme22eALTN  33818  cdleme42a  33944  cdleme42d  33946  cdlemk20  34347  dih1dimatlem0  34802  lcfrlem2  35017  elrfi  35442  fzsplit1nn0  35502  rabdiophlem2  35551  eldioph4b  35560  diophren  35562  pell1qrgaplem  35626  rngunsnply  35946  compne  36700  fmuldfeq  37538  limciccioolb  37578  ditgeq3d  37718  stoweidlem44  37782  dirkertrigeq  37840  fourierdlem32  37879  fourierdlem33  37880  fourierdlem42  37889  fourierdlem42OLD  37890  fourierdlem62  37909  fourierdlem84  37931  fourierdlem85  37932  fourierdlem97  37944  fourierdlem98  37945  fourierdlem102  37949  fourierdlem104  37951  fourierdlem113  37960  fourierdlem114  37961  fourierswlem  37971  fouriersw  37972  meadjun  38145  deccarry  38522  fsumsplitsndif  38860  funcrngcsetcALT  39586
  Copyright terms: Public domain W3C validator