Theorem syl5reqr 2485

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

Syntax hints:   -> wi 4   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431

This theorem is referenced by:  f0dom0  5590  f1o00  5668  fmpt  5859  fmptsn  5894  fninfp  5900  bm2.5ii  6412  frnsuppeq  6697  mapsn  7246  sbthlem4  7416  sbthlem6  7418  findcard2s  7545  elfiun  7672  cnfcom2  7927  cnfcom2OLD  7935  rankxplim3  8080  rankxpsuc  8081  pm54.43  8162  axdc3lem4  8614  gruun  8965  recmulnq  9125  reclem3pr  9210  xrmineq  11144  xadddi2  11252  iooval2  11325  hashsng  12128  hashfun  12191  hashbc  12198  isumclim3  13218  isummulc2  13221  ruclem4  13508  bitsshft  13663  phimullem  13846  pythagtriplem1  13875  1arithlem4  13979  fsets  14192  topnid  14366  pgrpsubgsymg  15904  odhash  16064  gsumzf1o  16382  gsumzf1oOLD  16385  pgpfaclem1  16570  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  evlslem4OLD  17565  evlslem4  17566  ordtrest2  18783  ufildr  19479  tsmsresOLD  19692  tsmsres  19693  rrxcph  20871  volinun  21002  uniioombllem4  21041  itg1climres  21167  limcco  21343  vieta1lem2  21752  coseq00topi  21939  tangtx  21942  coskpi  21957  advlog  22074  advlogexp  22075  logtayl  22080  logccv  22083  dvcxp1  22155  loglesqr  22171  ang180lem3  22182  dquart  22223  atans2  22301  basellem8  22400  chtub  22526  bposlem6  22603  lgsquadlem2  22669  logdivsum  22757  log2sumbnd  22768  ipval3  24055  siii  24204  cm2j  24974  pjssmii  25035  opsqrlem1  25495  hmopidmchi  25506  hmopidmpji  25507  pjcmul1i  25556  mddmd2  25664  cvexchlem  25723  dmdbr6ati  25778  difeq  25850  ffsrn  25980  ordtprsuni  26301  ordtrest2NEW  26305  zzsnm  26341  zzsnmOLD  26342  measun  26577  sxbrsigalem2  26653  eulerpartlemgu  26712  gsumnunsn  26889  signsplypnf  26903  cvmlift2lem12  27155  nepss  27325  fprodefsum  27436  iprodclim3  27451  bpolydiflem  28148  bpoly4  28153  ismblfin  28385  dvtan  28395  itg2addnclem3  28398  dvcncxp1  28430  dvasin  28433  dvacos  28434  dvreasin  28435  dvreacos  28436  areacirclem1  28437  diophrw  29050  wopprc  29332  fsuppeq  29403  zlmodzxzadd  30706  gsumdifsnd  30713  gsumdifsndf  30716  sineq0ALT  31560  glbconN  32861  pmodl42N  33335  2polssN  33399  cdleme20j  33802  trlcocnv  34204  trlcone  34212  lclkrlem2c  34994