Theorem syl5reqr 2448

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

Syntax hints:   -> wi 4   = wceq 1399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-ext 2370

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

This theorem is referenced by:  f0dom0  5690  f1o00  5769  fmpt  5967  fmptsn  6007  fninfp  6014  bm2.5ii  6558  frnsuppeq  6847  mapsn  7397  sbthlem4  7567  sbthlem6  7569  findcard2s  7694  elfiun  7823  cnfcom2  8077  cnfcom2OLD  8085  rankxplim3  8230  rankxpsuc  8231  pm54.43  8312  axdc3lem4  8764  gruun  9113  recmulnq  9271  reclem3pr  9356  xrmineq  11320  xadddi2  11428  iooval2  11501  hashsng  12360  hashfun  12418  hashbc  12425  isumclim3  13595  isummulc2  13598  iprodclim3  13814  fprodefsum  13851  ruclem4  13988  bitsshft  14146  phimullem  14330  pythagtriplem1  14361  1arithlem4  14465  fsets  14681  topnid  14862  pgrpsubgsymg  16569  odhash  16730  gsumzf1o  17053  gsumzf1oOLD  17056  gsumdifsnd  17120  pgpfaclem1  17264  mplcoe1  18259  mplcoe5  18263  mplcoe2OLD  18265  evlslem4OLD  18305  evlslem4  18306  ordtrest2  19810  ufildr  20536  tsmsresOLD  20749  tsmsres  20750  zlmclm  21699  rrxcph  21928  volinun  22060  uniioombllem4  22099  itg1climres  22225  limcco  22401  vieta1lem2  22811  coseq00topi  22999  tangtx  23002  coskpi  23017  advlog  23141  advlogexp  23142  logtayl  23147  logccv  23150  dvcxp1  23222  loglesqrt  23238  ang180lem3  23280  dquart  23319  atans2  23397  basellem8  23497  chtub  23623  bposlem6  23700  lgsquadlem2  23766  logdivsum  23854  log2sumbnd  23865  ipval3  25757  siii  25906  cm2j  26676  pjssmii  26737  opsqrlem1  27196  hmopidmchi  27207  hmopidmpji  27208  pjcmul1i  27257  mddmd2  27365  cvexchlem  27424  dmdbr6ati  27479  difeq  27557  ffsrn  27732  ordtprsuni  28086  ordtrest2NEW  28090  zzsnm  28126  measun  28374  sxbrsigalem2  28449  carsgsigalem  28478  eulerpartlemgu  28535  gsumnunsn  28712  signsplypnf  28726  cvmlift2lem12  28984  nepss  29297  bpolydiflem  30005  bpoly4  30010  ismblfin  30256  dvtan  30267  itg2addnclem3  30270  dvcncxp1  30302  dvasin  30305  dvacos  30306  dvreasin  30307  dvreacos  30308  areacirclem1  30309  diophrw  30893  wopprc  31174  fsuppeq  31245  iccdifioo  31756  itgvol0  31968  fourierdlem33  32123  etransclem32  32250  zlmodzxzadd  33182  gsumdifsndf  33190  sineq0ALT  34119  glbconN  35549  pmodl42N  36023  2polssN  36087  cdleme20j  36492  trlcocnv  36894  trlcone  36902  lclkrlem2c  37684