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

Theorem syl5req 2480
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 2479 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2440 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  syl5reqr  2482  opeqsn  4444  ordintdif  4622  relop  5014  funopg  5476  funcnvres  5513  nneob  6886  sucdom2  7294  unblem2  7351  pwfilem  7392  kmlem2  8020  kmlem11  8029  kmlem12  8030  cflim3  8131  1idsr  8962  recextlem1  9641  nn0supp  10262  quoremz  11224  quoremnn0ALT  11226  intfrac2  11227  hashprg  11654  hashfacen  11691  leiso  11696  cvgcmpce  12585  explecnv  12632  ramub1lem1  13382  ressress  13514  subsubc  14038  efginvrel2  15347  efgredleme  15363  efgcpbllemb  15375  frgpnabllem1  15472  gsumzmhm  15521  dprd2da  15588  dpjcntz  15598  dpjdisj  15599  dpjlsm  15600  dpjidcl  15604  ablfac1lem  15614  ablfac1eu  15619  lmhmlsp  16113  mplmon2mul  16549  neitr  17232  fixufil  17942  trust  18247  restmetu  18605  nmfval2  18626  nmval2  18627  rerest  18823  xrrest  18826  xrge0gsumle  18852  voliunlem3  19434  volsup  19438  itg1addlem5  19580  itg2monolem1  19630  itg2cnlem2  19642  itgmpt  19662  iblcnlem1  19667  itgcnlem  19669  itgioo  19695  limcres  19761  mdegfval  19973  dgrlem  20136  coeidlem  20144  mcubic  20675  binom4  20678  dquartlem2  20680  amgm  20817  wilthlem2  20840  rpvmasum2  21194  pntlemo  21289  wlkntrllem3  21549  opidon2  21900  vc2  22022  nvge0  22151  nmoo0  22280  bcsiALT  22669  pjchi  22922  shjshseli  22983  spanpr  23070  pjinvari  23682  mdslmd1lem2  23817  iundifdifd  24000  iundifdif  24001  gtiso  24076  esumpr2  24446  lgamgulmlem2  24802  eflgam  24817  risefallfac  25329  dvreasin  26226  topjoin  26331  tailfval  26338  tailf  26341  elrfi  26685  fzsplit1nn0  26749  rabdiophlem2  26799  eldioph4b  26809  diophren  26811  pell1qrgaplem  26873  rngunsnply  27293  psgnunilem1  27331  compne  27557  fmuldfeq  27627  stoweidlem44  27707  swrdccat3a  28105  frgrancvvdeqlem4  28280  cdleme4  30874  cdleme22e  30980  cdleme22eALTN  30981  cdleme42a  31107  cdleme42d  31109  cdlemk20  31510  dih1dimatlem0  31965  lcfrlem2  32180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator