Theorem syl5reqr 2507

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl5reqr.1	|- B = A
syl5reqr.2	|- ( ph -> B = C )

Assertion

Ref	Expression
syl5reqr	|- ( ph -> C = A )

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. . 3 |- B = A
2	1	eqcomi 2464	. 2 |- A = B
3		syl5reqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5req 2505	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-cleq 2443

This theorem is referenced by:  f0dom0  5696  f1o00  5774  fmpt  5966  fmptsn  6001  fninfp  6007  bm2.5ii  6520  frnsuppeq  6805  mapsn  7357  sbthlem4  7527  sbthlem6  7529  findcard2s  7657  elfiun  7784  cnfcom2  8039  cnfcom2OLD  8047  rankxplim3  8192  rankxpsuc  8193  pm54.43  8274  axdc3lem4  8726  gruun  9077  recmulnq  9237  reclem3pr  9322  xrmineq  11256  xadddi2  11364  iooval2  11437  hashsng  12246  hashfun  12310  hashbc  12317  isumclim3  13337  isummulc2  13340  ruclem4  13627  bitsshft  13782  phimullem  13965  pythagtriplem1  13994  1arithlem4  14098  fsets  14311  topnid  14485  pgrpsubgsymg  16024  odhash  16186  gsumzf1o  16504  gsumzf1oOLD  16507  pgpfaclem1  16696  mplcoe1  17660  mplcoe5  17664  mplcoe2OLD  17666  evlslem4OLD  17706  evlslem4  17707  ordtrest2  18933  ufildr  19629  tsmsresOLD  19842  tsmsres  19843  rrxcph  21021  volinun  21153  uniioombllem4  21192  itg1climres  21318  limcco  21494  vieta1lem2  21903  coseq00topi  22090  tangtx  22093  coskpi  22108  advlog  22225  advlogexp  22226  logtayl  22231  logccv  22234  dvcxp1  22306  loglesqr  22322  ang180lem3  22333  dquart  22374  atans2  22452  basellem8  22551  chtub  22677  bposlem6  22754  lgsquadlem2  22820  logdivsum  22908  log2sumbnd  22919  ipval3  24249  siii  24398  cm2j  25168  pjssmii  25229  opsqrlem1  25689  hmopidmchi  25700  hmopidmpji  25701  pjcmul1i  25750  mddmd2  25858  cvexchlem  25917  dmdbr6ati  25972  difeq  26044  ffsrn  26173  ordtprsuni  26487  ordtrest2NEW  26491  zzsnm  26527  zzsnmOLD  26528  measun  26763  sxbrsigalem2  26838  eulerpartlemgu  26897  gsumnunsn  27074  signsplypnf  27088  cvmlift2lem12  27340  nepss  27511  fprodefsum  27622  iprodclim3  27637  bpolydiflem  28334  bpoly4  28339  ismblfin  28573  dvtan  28583  itg2addnclem3  28586  dvcncxp1  28618  dvasin  28621  dvacos  28622  dvreasin  28623  dvreacos  28624  areacirclem1  28625  diophrw  29238  wopprc  29520  fsuppeq  29591  zlmodzxzadd  30896  gsumdifsnd  30903  gsumdifsndf  30906  sineq0ALT  31976  glbconN  33330  pmodl42N  33804  2polssN  33868  cdleme20j  34271  trlcocnv  34673  trlcone  34681  lclkrlem2c  35463