Theorem syl5reqr 2499

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

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

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

This theorem is referenced by:  f0dom0  5759  f1o00  5838  fmpt  6037  fmptsn  6076  fninfp  6083  bm2.5ii  6626  frnsuppeq  6915  mapsn  7462  sbthlem4  7632  sbthlem6  7634  findcard2s  7763  elfiun  7892  cnfcom2  8149  cnfcom2OLD  8157  rankxplim3  8302  rankxpsuc  8303  pm54.43  8384  axdc3lem4  8836  gruun  9187  recmulnq  9345  reclem3pr  9430  xrmineq  11392  xadddi2  11500  iooval2  11573  hashsng  12420  hashfun  12477  hashbc  12484  isumclim3  13556  isummulc2  13559  iprodclim3  13775  fprodefsum  13812  ruclem4  13949  bitsshft  14107  phimullem  14291  pythagtriplem1  14322  1arithlem4  14426  fsets  14640  topnid  14815  pgrpsubgsymg  16412  odhash  16573  gsumzf1o  16896  gsumzf1oOLD  16899  gsumdifsnd  16966  pgpfaclem1  17111  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  evlslem4OLD  18152  evlslem4  18153  ordtrest2  19683  ufildr  20410  tsmsresOLD  20623  tsmsres  20624  zlmclm  21573  rrxcph  21802  volinun  21934  uniioombllem4  21973  itg1climres  22099  limcco  22275  vieta1lem2  22685  coseq00topi  22873  tangtx  22876  coskpi  22891  advlog  23013  advlogexp  23014  logtayl  23019  logccv  23022  dvcxp1  23094  loglesqrt  23110  ang180lem3  23121  dquart  23162  atans2  23240  basellem8  23339  chtub  23465  bposlem6  23542  lgsquadlem2  23608  logdivsum  23696  log2sumbnd  23707  ipval3  25597  siii  25746  cm2j  26516  pjssmii  26577  opsqrlem1  27037  hmopidmchi  27048  hmopidmpji  27049  pjcmul1i  27098  mddmd2  27206  cvexchlem  27265  dmdbr6ati  27320  difeq  27394  ffsrn  27530  ordtprsuni  27879  ordtrest2NEW  27883  zzsnm  27919  zzsnmOLD  27920  measun  28160  sxbrsigalem2  28235  eulerpartlemgu  28294  gsumnunsn  28471  signsplypnf  28485  cvmlift2lem12  28737  nepss  29073  bpolydiflem  29792  bpoly4  29797  ismblfin  30031  dvtan  30041  itg2addnclem3  30044  dvcncxp1  30076  dvasin  30079  dvacos  30080  dvreasin  30081  dvreacos  30082  areacirclem1  30083  diophrw  30668  wopprc  30948  fsuppeq  31019  iccdifioo  31509  itgvol0  31721  fourierdlem33  31876  zlmodzxzadd  32815  gsumdifsndf  32823  sineq0ALT  33605  glbconN  34976  pmodl42N  35450  2polssN  35514  cdleme20j  35919  trlcocnv  36321  trlcone  36329  lclkrlem2c  37111