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

Theorem syl5req 2453
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 2452 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2413 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  syl5reqr  2455  opeqsn  4416  ordintdif  4594  relop  4986  funopg  5448  funcnvres  5485  nneob  6858  sucdom2  7266  unblem2  7323  pwfilem  7363  kmlem2  7991  kmlem11  8000  kmlem12  8001  cflim3  8102  1idsr  8933  recextlem1  9612  nn0supp  10233  quoremz  11195  quoremnn0ALT  11197  intfrac2  11198  hashprg  11625  hashfacen  11662  leiso  11667  cvgcmpce  12556  explecnv  12603  ramub1lem1  13353  ressress  13485  subsubc  14009  efginvrel2  15318  efgredleme  15334  efgcpbllemb  15346  frgpnabllem1  15443  gsumzmhm  15492  dprd2da  15559  dpjcntz  15569  dpjdisj  15570  dpjlsm  15571  dpjidcl  15575  ablfac1lem  15585  ablfac1eu  15590  lmhmlsp  16084  mplmon2mul  16520  neitr  17202  fixufil  17911  trust  18216  restmetu  18574  nmfval2  18595  nmval2  18596  rerest  18792  xrrest  18795  xrge0gsumle  18821  voliunlem3  19403  volsup  19407  itg1addlem5  19549  itg2monolem1  19599  itg2cnlem2  19611  itgmpt  19631  iblcnlem1  19636  itgcnlem  19638  itgioo  19664  limcres  19730  mdegfval  19942  dgrlem  20105  coeidlem  20113  mcubic  20644  binom4  20647  dquartlem2  20649  amgm  20786  wilthlem2  20809  rpvmasum2  21163  pntlemo  21258  wlkntrllem3  21518  opidon2  21869  vc2  21991  nvge0  22120  nmoo0  22249  bcsiALT  22638  pjchi  22891  shjshseli  22952  spanpr  23039  pjinvari  23651  mdslmd1lem2  23786  iundifdifd  23969  iundifdif  23970  gtiso  24045  esumpr2  24415  lgamgulmlem2  24771  eflgam  24786  risefallfac  25296  dvreasin  26183  topjoin  26288  tailfval  26295  tailf  26298  elrfi  26642  fzsplit1nn0  26706  rabdiophlem2  26756  eldioph4b  26766  diophren  26768  pell1qrgaplem  26830  rngunsnply  27250  psgnunilem1  27288  compne  27514  fmuldfeq  27584  stoweidlem44  27664  swrdccat3a  28034  frgrancvvdeqlem4  28140  cdleme4  30724  cdleme22e  30830  cdleme22eALTN  30831  cdleme42a  30957  cdleme42d  30959  cdlemk20  31360  dih1dimatlem0  31815  lcfrlem2  32030
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2401
  Copyright terms: Public domain W3C validator