Theorem syl5reqr 2451

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 2408	. 2 |- A = B
3		syl5reqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5req 2449	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1649

This theorem is referenced by:  bm2.5ii  4745  f1o00  5669  fmpt  5849  fmptsn  5881  mapsn  7014  sbthlem4  7179  sbthlem6  7181  findcard2s  7308  elfiun  7393  cnfcom2  7615  rankxplim3  7761  rankxpsuc  7762  pm54.43  7843  axdc3lem4  8289  gruun  8637  recmulnq  8797  reclem3pr  8882  xrmineq  10724  xadddi2  10832  iooval2  10905  hashsng  11602  hashfun  11655  hashbc  11657  isumclim3  12498  isummulc2  12501  ruclem4  12788  bitsshft  12942  phimullem  13123  pythagtriplem1  13145  1arithlem4  13249  topnid  13618  odhash  15163  gsumzf1o  15474  pgpfaclem1  15594  mplcoe1  16483  mplcoe2  16485  evlslem4  16519  ordtrest2  17222  ufildr  17916  tsmsres  18126  volinun  19393  uniioombllem4  19431  itg1climres  19559  limcco  19733  vieta1lem2  20181  coseq00topi  20363  tangtx  20366  coskpi  20381  advlog  20498  advlogexp  20499  logtayl  20504  logccv  20507  dvcxp1  20579  loglesqr  20595  ang180lem3  20606  dquart  20646  atans2  20724  basellem8  20823  chtub  20949  bposlem6  21026  lgsquadlem2  21092  logdivsum  21180  log2sumbnd  21191  ipval3  22158  siii  22307  cm2j  23075  pjssmii  23136  opsqrlem1  23596  hmopidmchi  23607  hmopidmpji  23608  pjcmul1i  23657  mddmd2  23765  cvexchlem  23824  dmdbr6ati  23879  difeq  23951  zzsnm  24295  measun  24518  sxbrsigalem2  24589  cvmlift2lem12  24954  nepss  25128  fprodefsum  25251  iprodclim3  25266  bpolydiflem  26004  bpoly4  26009  ismblfin  26146  itg2addnclem3  26157  dvreasin  26179  dvreacos  26180  areacirclem2  26181  fninfp  26625  diophrw  26707  wopprc  26991  fsuppeq  27127  glbconN  29859  pmodl42N  30333  2polssN  30397  cdleme20j  30800  trlcocnv  31202  trlcone  31210  lclkrlem2c  31992

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