Theorem syl5reqr 2523

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

Syntax hints:   -> wi 4   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

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

This theorem is referenced by:  f0dom0  5767  f1o00  5846  fmpt  6040  fmptsn  6079  fninfp  6086  bm2.5ii  6619  frnsuppeq  6910  mapsn  7457  sbthlem4  7627  sbthlem6  7629  findcard2s  7757  elfiun  7886  cnfcom2  8142  cnfcom2OLD  8150  rankxplim3  8295  rankxpsuc  8296  pm54.43  8377  axdc3lem4  8829  gruun  9180  recmulnq  9338  reclem3pr  9423  xrmineq  11377  xadddi2  11485  iooval2  11558  hashsng  12402  hashfun  12457  hashbc  12464  isumclim3  13533  isummulc2  13536  ruclem4  13824  bitsshft  13980  phimullem  14164  pythagtriplem1  14195  1arithlem4  14299  fsets  14512  topnid  14687  pgrpsubgsymg  16228  odhash  16390  gsumzf1o  16708  gsumzf1oOLD  16711  gsumdifsnd  16778  pgpfaclem1  16922  mplcoe1  17898  mplcoe5  17902  mplcoe2OLD  17904  evlslem4OLD  17944  evlslem4  17945  ordtrest2  19471  ufildr  20167  tsmsresOLD  20380  tsmsres  20381  rrxcph  21559  volinun  21691  uniioombllem4  21730  itg1climres  21856  limcco  22032  vieta1lem2  22441  coseq00topi  22628  tangtx  22631  coskpi  22646  advlog  22763  advlogexp  22764  logtayl  22769  logccv  22772  dvcxp1  22844  loglesqrt  22860  ang180lem3  22871  dquart  22912  atans2  22990  basellem8  23089  chtub  23215  bposlem6  23292  lgsquadlem2  23358  logdivsum  23446  log2sumbnd  23457  ipval3  25295  siii  25444  cm2j  26214  pjssmii  26275  opsqrlem1  26735  hmopidmchi  26746  hmopidmpji  26747  pjcmul1i  26796  mddmd2  26904  cvexchlem  26963  dmdbr6ati  27018  difeq  27090  ffsrn  27224  ordtprsuni  27537  ordtrest2NEW  27541  zzsnm  27577  zzsnmOLD  27578  measun  27822  sxbrsigalem2  27897  eulerpartlemgu  27956  gsumnunsn  28133  signsplypnf  28147  cvmlift2lem12  28399  nepss  28570  fprodefsum  28681  iprodclim3  28696  bpolydiflem  29393  bpoly4  29398  ismblfin  29632  dvtan  29642  itg2addnclem3  29645  dvcncxp1  29677  dvasin  29680  dvacos  29681  dvreasin  29682  dvreacos  29683  areacirclem1  29684  diophrw  30296  wopprc  30576  fsuppeq  30647  zlmodzxzadd  32011  gsumdifsndf  32020  sineq0ALT  32817  glbconN  34173  pmodl42N  34647  2polssN  34711  cdleme20j  35114  trlcocnv  35516  trlcone  35524  lclkrlem2c  36306