Theorem syl5req 2846

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

Hypotheses

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

Assertion

Ref	Expression
syl5req	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl5req

Step	Hyp	Ref	Expression
1		syl5req.1	. . 3 ⊢ 𝐴 = 𝐵
2		syl5req.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	syl5eq 2845	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2804	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  syl5reqr  2848  opeqsng  5358  relop  5685  ordintdif  6208  iotanul  6302  funopg  6358  funcnvres  6402  fpropnf1  7003  csbriota  7108  csbov123  7177  mpocurryd  7918  nneob  8262  sucdom2  8610  unblem2  8755  pwfilem  8802  kmlem2  9562  kmlem11  9571  kmlem12  9572  cflim3  9673  1idsr  10509  recextlem1  11259  quoremz  13218  quoremnn0ALT  13220  intfrac2  13221  hashprg  13752  hashfacen  13808  leiso  13813  ccatrid  13932  repsw2  14303  repsw3  14304  cvgcmpce  15165  explecnv  15212  risefallfac  15370  ramub1lem1  16352  ressress  16554  subsubc  17115  grp1inv  18199  symgplusg  18503  psgnunilem1  18613  psgn0fv0  18631  psgnsn  18640  efginvrel2  18845  efgredleme  18861  efgcpbllemb  18873  frgpnabllem1  18986  gsumzaddlem  19034  gsumzmhm  19050  fsfnn0gsumfsffz  19096  dprd2da  19157  dpjcntz  19167  dpjdisj  19168  dpjlsm  19169  dpjidcl  19173  ablfac1lem  19183  ablfac1eu  19188  rnrhmsubrg  19560  lmhmlsp  19814  frlmip  20467  mplmon2mul  20740  1marepvmarrepid  21180  m1detdiag  21202  cramerimplem2  21289  pmatcollpw3lem  21388  chpscmatgsumbin  21449  chpscmatgsummon  21450  cayhamlem2  21489  neitr  21785  fixufil  22527  trust  22835  restmetu  23177  nmfval2  23197  nmval2  23198  rerest  23409  xrrest  23412  xrge0gsumle  23438  rrxip  23994  rrx0  24001  rrxdsfi  24015  voliunlem3  24156  volsup  24160  itg1addlem5  24304  itg2monolem1  24354  itg2cnlem2  24366  itgmpt  24386  iblcnlem1  24391  itgcnlem  24393  itgioo  24419  limcres  24489  mdegfval  24663  dgrlem  24826  coeidlem  24834  mcubic  25433  binom4  25436  dquartlem2  25438  amgm  25576  lgamgulmlem2  25615  eflgam  25630  wilthlem2  25654  rpvmasum2  26096  pntlemo  26191  wlkres  27460  3wlkond  27956  3cycld  27963  frgrncvvdeqlem3  28086  vc2OLD  28351  nvge0  28456  nmoo0  28574  bcsiALT  28962  pjchi  29215  shjshseli  29276  spanpr  29363  pjinvari  29974  mdslmd1lem2  30109  iundifdifd  30325  iundifdif  30326  fmptco1f1o  30392  gtiso  30460  gsumhashmul  30741  cycpmco2lem4  30821  cycpmconjslem2  30847  rngurd  30907  rspsnel  30987  zarcls0  31221  esumpr2  31436  omssubaddlem  31667  eulerpartlemt  31739  ofcccat  31923  2cycld  32498  satfv1lem  32722  topjoin  33826  tailfval  33833  tailf  33836  dvasin  35141  dvacos  35142  opidon2OLD  35292  cdleme4  37534  cdleme22e  37640  cdleme22eALTN  37641  cdleme42a  37767  cdleme42d  37769  cdlemk20  38170  dih1dimatlem0  38624  lcfrlem2  38839  prjspnval2  39611  elrfi  39635  fzsplit1nn0  39695  rabdiophlem2  39743  eldioph4b  39752  diophren  39754  pell1qrgaplem  39814  rngunsnply  40117  disjinfi  41820  fmuldfeq  42225  limciccioolb  42263  ditgeq3d  42606  stoweidlem44  42686  dirkertrigeq  42743  fourierdlem32  42781  fourierdlem33  42782  fourierdlem42  42791  fourierdlem62  42810  fourierdlem84  42832  fourierdlem85  42833  fourierdlem97  42845  fourierdlem98  42846  fourierdlem102  42850  fourierdlem104  42852  fourierdlem113  42861  fourierdlem114  42862  fourierswlem  42872  fouriersw  42873  sssalgen  42975  meadjun  43101  deccarry  43868  fsumsplitsndif  43890  isomushgr  44344  ushrisomgr  44359  funcrngcsetcALT  44623  2sphere  45163