Theorem syl5reqr 2478

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

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-cleq 2414

This theorem is referenced by:  f0dom0  5784  f1o00  5863  fmpt  6058  fmptsn  6099  fninfp  6106  bm2.5ii  6647  frnsuppeq  6937  mapsn  7524  sbthlem4  7694  sbthlem6  7696  findcard2s  7821  elfiun  7953  cnfcom2  8215  rankxplim3  8360  rankxpsuc  8361  pm54.43  8442  axdc3lem4  8890  gruun  9238  recmulnq  9396  reclem3pr  9481  xrmineq  11482  xadddi2  11590  iooval2  11676  hashsng  12555  hashfun  12613  hashbc  12620  isumclim3  13819  isummulc2  13822  iprodclim3  14052  bpolydiflem  14106  bpoly4  14111  fprodefsum  14148  ruclem4  14285  bitsshft  14448  phimullem  14726  pythagtriplem1  14765  1arithlem4  14869  fsets  15148  topnid  15333  pgrpsubgsymg  17048  odhash  17222  gsumzf1o  17545  gsumdifsnd  17592  pgpfaclem1  17713  mplcoe1  18688  mplcoe5  18691  evlslem4  18730  ordtrest2  20218  ufildr  20944  tsmsres  21156  zlmclm  22124  rrxcph  22349  volinun  22497  uniioombllem4  22542  itg1climres  22670  limcco  22846  vieta1lem2  23262  coseq00topi  23455  tangtx  23458  coskpi  23473  advlog  23597  advlogexp  23598  logtayl  23603  logccv  23606  dvcxp1  23678  dvcncxp1  23681  loglesqrt  23696  ang180lem3  23738  dquart  23777  atans2  23855  basellem8  24012  chtub  24138  bposlem6  24215  lgsquadlem2  24281  logdivsum  24369  log2sumbnd  24380  ipval3  26343  siii  26492  cm2j  27271  pjssmii  27332  opsqrlem1  27791  hmopidmchi  27802  hmopidmpji  27803  pjcmul1i  27852  mddmd2  27960  cvexchlem  28019  dmdbr6ati  28074  difeq  28150  ffsrn  28320  ordtprsuni  28733  ordtrest2NEW  28737  zzsnm  28773  measun  29041  sxbrsigalem2  29116  carsgsigalem  29155  eulerpartlemgu  29218  gsumnunsn  29433  signsplypnf  29447  cvmlift2lem12  30045  nepss  30358  fwddifnp1  30937  finxpreclem1  31745  finxpreclem3  31749  poimirlem31  31935  ismblfin  31945  dvtan  31956  itg2addnclem3  31959  dvasin  31992  dvacos  31993  dvreasin  31994  dvreacos  31995  areacirclem1  31996  glbconN  32911  pmodl42N  33385  2polssN  33449  cdleme20j  33854  trlcocnv  34256  trlcone  34264  lclkrlem2c  35046  diophrw  35570  wopprc  35855  sineq0ALT  37307  iccdifioo  37565  itgvol0  37785  fourierdlem33  37943  etransclem32  38071  zlmodzxzadd  39760  gsumdifsndf  39768