Theorem syl5reqr 2501

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

Syntax hints:   -> wi 4   = wceq 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-cleq 2445

This theorem is referenced by:  f0dom0  5750  f1o00  5830  fmpt  6027  fmptsn  6069  fninfp  6076  bm2.5ii  6621  frnsuppeq  6914  mapsn  7500  sbthlem4  7672  sbthlem6  7674  findcard2s  7799  elfiun  7931  cnfcom2  8194  rankxplim3  8339  rankxpsuc  8340  pm54.43  8421  axdc3lem4  8870  gruun  9218  recmulnq  9376  reclem3pr  9461  xrmineq  11465  xadddi2  11573  iooval2  11659  hashsng  12543  hashfun  12604  hashbc  12611  isumclim3  13831  isummulc2  13834  iprodclim3  14064  bpolydiflem  14118  bpoly4  14123  fprodefsum  14160  ruclem4  14297  bitsshft  14460  phimullem  14738  pythagtriplem1  14777  1arithlem4  14881  fsets  15160  topnid  15345  pgrpsubgsymg  17060  odhash  17234  gsumzf1o  17557  gsumdifsnd  17604  pgpfaclem1  17725  mplcoe1  18700  mplcoe5  18703  evlslem4  18742  ordtrest2  20231  ufildr  20957  tsmsres  21169  zlmclm  22137  rrxcph  22362  volinun  22511  uniioombllem4  22556  itg1climres  22684  limcco  22860  vieta1lem2  23276  coseq00topi  23469  tangtx  23472  coskpi  23487  advlog  23611  advlogexp  23612  logtayl  23617  logccv  23620  dvcxp1  23692  dvcncxp1  23695  loglesqrt  23710  ang180lem3  23752  dquart  23791  atans2  23869  basellem8  24026  chtub  24152  bposlem6  24229  lgsquadlem2  24295  logdivsum  24383  log2sumbnd  24394  ipval3  26357  siii  26506  cm2j  27285  pjssmii  27346  opsqrlem1  27805  hmopidmchi  27816  hmopidmpji  27817  pjcmul1i  27866  mddmd2  27974  cvexchlem  28033  dmdbr6ati  28088  difeq  28163  ffsrn  28322  ordtprsuni  28732  ordtrest2NEW  28736  zzsnm  28772  measun  29040  sxbrsigalem2  29114  carsgsigalem  29153  eulerpartlemgu  29216  gsumnunsn  29431  signsplypnf  29445  cvmlift2lem12  30043  nepss  30356  fwddifnp1  30938  finxpreclem1  31783  finxpreclem3  31787  poimirlem31  31973  ismblfin  31983  dvtan  31994  itg2addnclem3  31997  dvasin  32030  dvacos  32031  dvreasin  32032  dvreacos  32033  areacirclem1  32034  glbconN  32944  pmodl42N  33418  2polssN  33482  cdleme20j  33887  trlcocnv  34289  trlcone  34297  lclkrlem2c  35079  diophrw  35603  wopprc  35887  sineq0ALT  37331  mapsnd  37486  iccdifioo  37657  itgvol0  37887  fourierdlem33  38060  etransclem32  38188  sPthisPth  39812  zlmodzxzadd  40464  gsumdifsndf  40472