Theorem syl5reqr 2480

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

Syntax hints:   -> wi 4   = wceq 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-cleq 2426

This theorem is referenced by:  f0dom0  5583  f1o00  5661  fmpt  5852  fmptsn  5886  fninfp  5892  bm2.5ii  6406  frnsuppeq  6691  mapsn  7242  sbthlem4  7412  sbthlem6  7414  findcard2s  7541  elfiun  7668  cnfcom2  7923  cnfcom2OLD  7931  rankxplim3  8076  rankxpsuc  8077  pm54.43  8158  axdc3lem4  8610  gruun  8960  recmulnq  9120  reclem3pr  9205  xrmineq  11139  xadddi2  11247  iooval2  11320  hashsng  12119  hashfun  12182  hashbc  12189  isumclim3  13209  isummulc2  13212  ruclem4  13498  bitsshft  13653  phimullem  13836  pythagtriplem1  13865  1arithlem4  13969  fsets  14182  topnid  14356  pgrpsubgsymg  15892  odhash  16052  gsumzf1o  16370  gsumzf1oOLD  16373  pgpfaclem1  16555  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  evlslem4OLD  17517  evlslem4  17518  ordtrest2  18649  ufildr  19345  tsmsresOLD  19558  tsmsres  19559  rrxcph  20737  volinun  20868  uniioombllem4  20907  itg1climres  21033  limcco  21209  vieta1lem2  21661  coseq00topi  21848  tangtx  21851  coskpi  21866  advlog  21983  advlogexp  21984  logtayl  21989  logccv  21992  dvcxp1  22064  loglesqr  22080  ang180lem3  22091  dquart  22132  atans2  22210  basellem8  22309  chtub  22435  bposlem6  22512  lgsquadlem2  22578  logdivsum  22666  log2sumbnd  22677  ipval3  23926  siii  24075  cm2j  24845  pjssmii  24906  opsqrlem1  25366  hmopidmchi  25377  hmopidmpji  25378  pjcmul1i  25427  mddmd2  25535  cvexchlem  25594  dmdbr6ati  25649  difeq  25722  ffsrn  25853  ordtprsuni  26202  ordtrest2NEW  26206  zzsnm  26242  zzsnmOLD  26243  measun  26478  sxbrsigalem2  26554  eulerpartlemgu  26607  gsumnunsn  26784  signsplypnf  26798  cvmlift2lem12  27050  nepss  27220  fprodefsum  27331  iprodclim3  27346  bpolydiflem  28043  bpoly4  28048  ismblfin  28273  dvtan  28283  itg2addnclem3  28286  dvcncxp1  28318  dvasin  28321  dvacos  28322  dvreasin  28323  dvreacos  28324  areacirclem1  28325  diophrw  28939  wopprc  29221  fsuppeq  29292  zlmodzxzadd  30586  gsumdifsnd  30593  sineq0ALT  31372  glbconN  32591  pmodl42N  33065  2polssN  33129  cdleme20j  33532  trlcocnv  33934  trlcone  33942  lclkrlem2c  34724