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

Theorem syl5req 2425
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 2424 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2385 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  syl5reqr  2427  opeqsn  4386  ordintdif  4564  relop  4956  funopg  5418  funcnvres  5455  nneob  6824  sucdom2  7232  unblem2  7289  pwfilem  7329  kmlem2  7957  kmlem11  7966  kmlem12  7967  cflim3  8068  1idsr  8899  recextlem1  9577  nn0supp  10198  quoremz  11156  quoremnn0ALT  11158  intfrac2  11159  hashprg  11586  hashfacen  11623  leiso  11628  cvgcmpce  12517  explecnv  12564  ramub1lem1  13314  ressress  13446  subsubc  13970  efginvrel2  15279  efgredleme  15295  efgcpbllemb  15307  frgpnabllem1  15404  gsumzmhm  15453  dprd2da  15520  dpjcntz  15530  dpjdisj  15531  dpjlsm  15532  dpjidcl  15536  ablfac1lem  15546  ablfac1eu  15551  lmhmlsp  16045  mplmon2mul  16481  neitr  17159  fixufil  17868  trust  18173  restmetu  18482  nmfval2  18502  nmval2  18503  rerest  18699  xrrest  18702  xrge0gsumle  18728  voliunlem3  19306  volsup  19310  itg1addlem5  19452  itg2monolem1  19502  itg2cnlem2  19514  itgmpt  19534  iblcnlem1  19539  itgcnlem  19541  itgioo  19567  limcres  19633  mdegfval  19845  dgrlem  20008  coeidlem  20016  mcubic  20547  binom4  20550  dquartlem2  20552  amgm  20689  wilthlem2  20712  rpvmasum2  21066  pntlemo  21161  wlkntrllem5  21410  opidon2  21753  vc2  21875  nvge0  22004  nmoo0  22133  bcsiALT  22522  pjchi  22775  shjshseli  22836  spanpr  22923  pjinvari  23535  mdslmd1lem2  23670  iundifdifd  23849  iundifdif  23850  gtiso  23922  esumpr2  24247  lgamgulmlem2  24586  eflgam  24601  risefallfac  25101  dvreasin  25973  topjoin  26078  tailfval  26085  tailf  26088  elrfi  26432  fzsplit1nn0  26496  rabdiophlem2  26546  eldioph4b  26556  diophren  26558  pell1qrgaplem  26620  rngunsnply  27040  psgnunilem1  27078  compne  27304  fmuldfeq  27374  stoweidlem44  27454  frgrancvvdeqlem4  27778  cdleme4  30403  cdleme22e  30509  cdleme22eALTN  30510  cdleme42a  30636  cdleme42d  30638  cdlemk20  31039  dih1dimatlem0  31494  lcfrlem2  31709
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 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2373
  Copyright terms: Public domain W3C validator