Theorem syl5reqr 2671

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

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  resdmdfsn  5445  f0dom0  6089  f1o00  6171  fmpt  6381  fmptsn  6433  fninfp  6440  bm2.5ii  7006  frnsuppeq  7307  mapsn  7899  sbthlem4  8073  sbthlem6  8075  findcard2s  8201  elfiun  8336  cnfcom2  8599  rankxplim3  8744  rankxpsuc  8745  pm54.43  8826  axdc3lem4  9275  gruun  9628  recmulnq  9786  reclem3pr  9871  xrmineq  12011  xadddi2  12127  iooval2  12208  hashsng  13159  hashfun  13224  hashbc  13237  isumclim3  14490  isummulc2  14493  iprodclim3  14731  bpolydiflem  14785  bpoly4  14790  fprodefsum  14825  ruclem4  14963  bitsshft  15197  phimullem  15484  pythagtriplem1  15521  1arithlem4  15630  fsets  15891  topnid  16096  pgrpsubgsymg  17828  odhash  17989  gsumzf1o  18313  gsumdifsnd  18360  pgpfaclem1  18480  mplcoe1  19465  mplcoe5  19468  evlslem4  19508  ordtrest2  21008  ufildr  21735  tsmsres  21947  zlmclm  22912  cphipval2  23040  rrxcph  23180  volinun  23314  uniioombllem4  23354  itg1climres  23481  limcco  23657  vieta1lem2  24066  coseq00topi  24254  tangtx  24257  coskpi  24272  advlog  24400  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  dvcncxp1  24484  loglesqrt  24499  ang180lem3  24541  dquart  24580  atans2  24658  basellem8  24814  chtub  24937  bposlem6  25014  lgsquadlem2  25106  logdivsum  25222  log2sumbnd  25233  spthispth  26622  ipval3  27564  siii  27708  cm2j  28479  pjssmii  28540  opsqrlem1  28999  hmopidmchi  29010  hmopidmpji  29011  pjcmul1i  29060  mddmd2  29168  cvexchlem  29227  dmdbr6ati  29282  difeq  29355  difuncomp  29369  ffsrn  29504  ordtprsuni  29965  ordtrest2NEW  29969  zzsnm  30005  measun  30274  sxbrsigalem2  30348  carsgsigalem  30377  eulerpartlemgu  30439  gsumnunsn  30615  signsplypnf  30627  logdivsqrle  30728  cvmlift2lem12  31296  nepss  31599  nodenselem5  31838  fwddifnp1  32272  finxpreclem1  33226  finxpreclem3  33230  poimirlem31  33440  ismblfin  33450  dvtan  33460  itg2addnclem3  33463  dvasin  33496  dvacos  33497  dvreasin  33498  dvreacos  33499  areacirclem1  33500  glbconN  34663  pmodl42N  35137  2polssN  35201  cdleme20j  35606  trlcocnv  36008  trlcone  36016  lclkrlem2c  36798  diophrw  37322  wopprc  37597  fsovcnvlem  38307  sineq0ALT  39173  mapsnd  39388  iccdifioo  39741  itgvol0  40184  fourierdlem33  40357  etransclem32  40483  zlmodzxzadd  42136  gsumdifsndf  42144