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

Theorem syl5req 2449
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 2448 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2409 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  syl5reqr  2451  opeqsn  4412  ordintdif  4590  relop  4982  funopg  5444  funcnvres  5481  nneob  6854  sucdom2  7262  unblem2  7319  pwfilem  7359  kmlem2  7987  kmlem11  7996  kmlem12  7997  cflim3  8098  1idsr  8929  recextlem1  9608  nn0supp  10229  quoremz  11191  quoremnn0ALT  11193  intfrac2  11194  hashprg  11621  hashfacen  11658  leiso  11663  cvgcmpce  12552  explecnv  12599  ramub1lem1  13349  ressress  13481  subsubc  14005  efginvrel2  15314  efgredleme  15330  efgcpbllemb  15342  frgpnabllem1  15439  gsumzmhm  15488  dprd2da  15555  dpjcntz  15565  dpjdisj  15566  dpjlsm  15567  dpjidcl  15571  ablfac1lem  15581  ablfac1eu  15586  lmhmlsp  16080  mplmon2mul  16516  neitr  17198  fixufil  17907  trust  18212  restmetu  18570  nmfval2  18591  nmval2  18592  rerest  18788  xrrest  18791  xrge0gsumle  18817  voliunlem3  19399  volsup  19403  itg1addlem5  19545  itg2monolem1  19595  itg2cnlem2  19607  itgmpt  19627  iblcnlem1  19632  itgcnlem  19634  itgioo  19660  limcres  19726  mdegfval  19938  dgrlem  20101  coeidlem  20109  mcubic  20640  binom4  20643  dquartlem2  20645  amgm  20782  wilthlem2  20805  rpvmasum2  21159  pntlemo  21254  wlkntrllem3  21514  opidon2  21865  vc2  21987  nvge0  22116  nmoo0  22245  bcsiALT  22634  pjchi  22887  shjshseli  22948  spanpr  23035  pjinvari  23647  mdslmd1lem2  23782  iundifdifd  23965  iundifdif  23966  gtiso  24041  esumpr2  24411  lgamgulmlem2  24767  eflgam  24782  risefallfac  25292  dvreasin  26179  topjoin  26284  tailfval  26291  tailf  26294  elrfi  26638  fzsplit1nn0  26702  rabdiophlem2  26752  eldioph4b  26762  diophren  26764  pell1qrgaplem  26826  rngunsnply  27246  psgnunilem1  27284  compne  27510  fmuldfeq  27580  stoweidlem44  27660  swrdccat3a  28030  frgrancvvdeqlem4  28136  cdleme4  30720  cdleme22e  30826  cdleme22eALTN  30827  cdleme42a  30953  cdleme42d  30955  cdlemk20  31356  dih1dimatlem0  31811  lcfrlem2  32026
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 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator