Theorem syl5reqr 2659

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl5reqr.1	⊢ 𝐵 = 𝐴
syl5reqr.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
syl5reqr	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2619	. 2 ⊢ 𝐴 = 𝐵
3		syl5reqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5req 2657	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  resdmdfsn  5365  f0dom0  6002  f1o00  6083  fmpt  6289  fmptsn  6338  fninfp  6345  bm2.5ii  6898  frnsuppeq  7194  mapsn  7785  sbthlem4  7958  sbthlem6  7960  findcard2s  8086  elfiun  8219  cnfcom2  8482  rankxplim3  8627  rankxpsuc  8628  pm54.43  8709  axdc3lem4  9158  gruun  9507  recmulnq  9665  reclem3pr  9750  xrmineq  11885  xadddi2  11999  iooval2  12079  hashsng  13020  hashfun  13084  hashbc  13094  isumclim3  14332  isummulc2  14335  iprodclim3  14570  bpolydiflem  14624  bpoly4  14629  fprodefsum  14664  ruclem4  14802  bitsshft  15035  phimullem  15322  pythagtriplem1  15359  1arithlem4  15468  fsets  15723  topnid  15919  pgrpsubgsymg  17651  odhash  17812  gsumzf1o  18136  gsumdifsnd  18183  pgpfaclem1  18303  mplcoe1  19286  mplcoe5  19289  evlslem4  19329  ordtrest2  20818  ufildr  21545  tsmsres  21757  zlmclm  22720  cphipval2  22848  rrxcph  22988  volinun  23121  uniioombllem4  23160  itg1climres  23287  limcco  23463  vieta1lem2  23870  coseq00topi  24058  tangtx  24061  coskpi  24076  advlog  24200  advlogexp  24201  logtayl  24206  logccv  24209  dvcxp1  24281  dvcncxp1  24284  loglesqrt  24299  ang180lem3  24341  dquart  24380  atans2  24458  basellem8  24614  chtub  24737  bposlem6  24814  lgsquadlem2  24906  logdivsum  25022  log2sumbnd  25033  ipval3  26948  siii  27092  cm2j  27863  pjssmii  27924  opsqrlem1  28383  hmopidmchi  28394  hmopidmpji  28395  pjcmul1i  28444  mddmd2  28552  cvexchlem  28611  dmdbr6ati  28666  difeq  28739  difuncomp  28752  ffsrn  28892  ordtprsuni  29293  ordtrest2NEW  29297  zzsnm  29333  measun  29601  sxbrsigalem2  29675  carsgsigalem  29704  eulerpartlemgu  29766  gsumnunsn  29942  signsplypnf  29953  cvmlift2lem12  30550  nepss  30854  fwddifnp1  31442  finxpreclem1  32402  finxpreclem3  32406  poimirlem31  32610  ismblfin  32620  dvtan  32630  itg2addnclem3  32633  dvasin  32666  dvacos  32667  dvreasin  32668  dvreacos  32669  areacirclem1  32670  glbconN  33681  pmodl42N  34155  2polssN  34219  cdleme20j  34624  trlcocnv  35026  trlcone  35034  lclkrlem2c  35816  diophrw  36340  wopprc  36615  fsovcnvlem  37327  sineq0ALT  38195  mapsnd  38383  iccdifioo  38588  itgvol0  38860  fourierdlem33  39033  etransclem32  39159  sPthisPth  40932  zlmodzxzadd  41929  gsumdifsndf  41937