Theorem syl5req 2869

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 2868	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2827	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  syl5reqr  2871  opeqsng  5393  relop  5721  ordintdif  6240  iotanul  6333  funopg  6389  funcnvres  6432  fpropnf1  7025  csbriota  7129  csbov123  7198  mpocurryd  7935  nneob  8279  sucdom2  8714  unblem2  8771  pwfilem  8818  kmlem2  9577  kmlem11  9586  kmlem12  9587  cflim3  9684  1idsr  10520  recextlem1  11270  quoremz  13224  quoremnn0ALT  13226  intfrac2  13227  hashprg  13757  hashfacen  13813  leiso  13818  ccatrid  13941  repsw2  14312  repsw3  14313  cvgcmpce  15173  explecnv  15220  risefallfac  15378  ramub1lem1  16362  ressress  16562  subsubc  17123  grp1inv  18207  symgplusg  18511  psgnunilem1  18621  psgn0fv0  18639  psgnsn  18648  efginvrel2  18853  efgredleme  18869  efgcpbllemb  18881  frgpnabllem1  18993  gsumzaddlem  19041  gsumzmhm  19057  fsfnn0gsumfsffz  19103  dprd2da  19164  dpjcntz  19174  dpjdisj  19175  dpjlsm  19176  dpjidcl  19180  ablfac1lem  19190  ablfac1eu  19195  rnrhmsubrg  19567  lmhmlsp  19821  mplmon2mul  20281  frlmip  20922  1marepvmarrepid  21184  m1detdiag  21206  cramerimplem2  21293  pmatcollpw3lem  21391  chpscmatgsumbin  21452  chpscmatgsummon  21453  cayhamlem2  21492  neitr  21788  fixufil  22530  trust  22838  restmetu  23180  nmfval2  23200  nmval2  23201  rerest  23412  xrrest  23415  xrge0gsumle  23441  rrxip  23993  rrx0  24000  rrxdsfi  24014  voliunlem3  24153  volsup  24157  itg1addlem5  24301  itg2monolem1  24351  itg2cnlem2  24363  itgmpt  24383  iblcnlem1  24388  itgcnlem  24390  itgioo  24416  limcres  24484  mdegfval  24656  dgrlem  24819  coeidlem  24827  mcubic  25425  binom4  25428  dquartlem2  25430  amgm  25568  lgamgulmlem2  25607  eflgam  25622  wilthlem2  25646  rpvmasum2  26088  pntlemo  26183  wlkres  27452  3wlkond  27950  3cycld  27957  frgrncvvdeqlem3  28080  vc2OLD  28345  nvge0  28450  nmoo0  28568  bcsiALT  28956  pjchi  29209  shjshseli  29270  spanpr  29357  pjinvari  29968  mdslmd1lem2  30103  iundifdifd  30313  iundifdif  30314  fmptco1f1o  30378  gtiso  30436  cycpmco2lem4  30771  cycpmconjslem2  30797  rngurd  30857  rspsnel  30936  esumpr2  31326  omssubaddlem  31557  eulerpartlemt  31629  ofcccat  31813  2cycld  32385  satfv1lem  32609  topjoin  33713  tailfval  33720  tailf  33723  dvasin  34993  dvacos  34994  opidon2OLD  35147  cdleme4  37389  cdleme22e  37495  cdleme22eALTN  37496  cdleme42a  37622  cdleme42d  37624  cdlemk20  38025  dih1dimatlem0  38479  lcfrlem2  38694  prjspnval2  39316  elrfi  39340  fzsplit1nn0  39400  rabdiophlem2  39448  eldioph4b  39457  diophren  39459  pell1qrgaplem  39519  rngunsnply  39822  fmuldfeq  41913  limciccioolb  41951  ditgeq3d  42298  stoweidlem44  42378  dirkertrigeq  42435  fourierdlem32  42473  fourierdlem33  42474  fourierdlem42  42483  fourierdlem62  42502  fourierdlem84  42524  fourierdlem85  42525  fourierdlem97  42537  fourierdlem98  42538  fourierdlem102  42542  fourierdlem104  42544  fourierdlem113  42553  fourierdlem114  42554  fourierswlem  42564  fouriersw  42565  sssalgen  42667  meadjun  42793  deccarry  43560  fsumsplitsndif  43582  isomushgr  44040  ushrisomgr  44055  funcrngcsetcALT  44319  2sphere  44785