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

Theorem syl5req 2483
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 2482 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2443 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  syl5reqr  2485  opeqsn  4455  ordintdif  4633  relop  5026  funopg  5488  funcnvres  5525  nneob  6898  sucdom2  7306  unblem2  7363  pwfilem  7404  kmlem2  8036  kmlem11  8045  kmlem12  8046  cflim3  8147  1idsr  8978  recextlem1  9657  nn0supp  10278  quoremz  11241  quoremnn0ALT  11243  intfrac2  11244  hashprg  11671  hashfacen  11708  leiso  11713  cvgcmpce  12602  explecnv  12649  ramub1lem1  13399  ressress  13531  subsubc  14055  efginvrel2  15364  efgredleme  15380  efgcpbllemb  15392  frgpnabllem1  15489  gsumzmhm  15538  dprd2da  15605  dpjcntz  15615  dpjdisj  15616  dpjlsm  15617  dpjidcl  15621  ablfac1lem  15631  ablfac1eu  15636  lmhmlsp  16130  mplmon2mul  16566  neitr  17249  fixufil  17959  trust  18264  restmetu  18622  nmfval2  18643  nmval2  18644  rerest  18840  xrrest  18843  xrge0gsumle  18869  voliunlem3  19451  volsup  19455  itg1addlem5  19595  itg2monolem1  19645  itg2cnlem2  19657  itgmpt  19677  iblcnlem1  19682  itgcnlem  19684  itgioo  19710  limcres  19778  mdegfval  19990  dgrlem  20153  coeidlem  20161  mcubic  20692  binom4  20695  dquartlem2  20697  amgm  20834  wilthlem2  20857  rpvmasum2  21211  pntlemo  21306  wlkntrllem3  21566  opidon2  21917  vc2  22039  nvge0  22168  nmoo0  22297  bcsiALT  22686  pjchi  22939  shjshseli  23000  spanpr  23087  pjinvari  23699  mdslmd1lem2  23834  iundifdifd  24017  iundifdif  24018  gtiso  24093  esumpr2  24463  lgamgulmlem2  24819  eflgam  24834  risefallfac  25345  dvreasin  26304  topjoin  26408  tailfval  26415  tailf  26418  elrfi  26762  fzsplit1nn0  26826  rabdiophlem2  26876  eldioph4b  26886  diophren  26888  pell1qrgaplem  26950  rngunsnply  27369  psgnunilem1  27407  compne  27633  fmuldfeq  27703  stoweidlem44  27783  swrdccat3a  28251  frgrancvvdeqlem4  28496  cdleme4  31109  cdleme22e  31215  cdleme22eALTN  31216  cdleme42a  31342  cdleme42d  31344  cdlemk20  31745  dih1dimatlem0  32200  lcfrlem2  32415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator