Theorem syl5req 2657

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 2656	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2616	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:  syl5reqr  2659  opeqsn  4892  relop  5194  ordintdif  5691  funopg  5836  funcnvres  5881  csbriota  6523  csbov123  6585  mpt2curryd  7282  nneob  7619  sucdom2  8041  unblem2  8098  pwfilem  8143  kmlem2  8856  kmlem11  8865  kmlem12  8866  cflim3  8967  1idsr  9798  recextlem1  10536  quoremz  12516  quoremnn0ALT  12518  intfrac2  12519  hashprg  13043  hashprgOLD  13044  hashfacen  13095  leiso  13100  ccatrid  13223  swrdccat3a  13345  repsw2  13541  repsw3  13542  cvgcmpce  14391  explecnv  14436  risefallfac  14594  ramub1lem1  15568  ressress  15765  subsubc  16336  grp1inv  17346  psgnunilem1  17736  psgn0fv0  17754  psgnsn  17763  efginvrel2  17963  efgredleme  17979  efgcpbllemb  17991  frgpnabllem1  18099  gsumzaddlem  18144  gsumzmhm  18160  fsfnn0gsumfsffz  18202  dprd2da  18264  dpjcntz  18274  dpjdisj  18275  dpjlsm  18276  dpjidcl  18280  ablfac1lem  18290  ablfac1eu  18295  lmhmlsp  18870  mplmon2mul  19322  frlmip  19936  1marepvmarrepid  20200  m1detdiag  20222  cramerimplem2  20309  pmatcollpw3lem  20407  chpscmatgsumbin  20468  chpscmatgsummon  20469  cayhamlem2  20508  neitr  20794  fixufil  21536  trust  21843  restmetu  22185  nmfval2  22205  nmval2  22206  rerest  22415  xrrest  22418  xrge0gsumle  22444  rrxip  22986  voliunlem3  23127  volsup  23131  itg1addlem5  23273  itg2monolem1  23323  itg2cnlem2  23335  itgmpt  23355  iblcnlem1  23360  itgcnlem  23362  itgioo  23388  limcres  23456  mdegfval  23626  dgrlem  23789  coeidlem  23797  mcubic  24374  binom4  24377  dquartlem2  24379  amgm  24517  lgamgulmlem2  24556  eflgam  24571  wilthlem2  24595  rpvmasum2  25001  pntlemo  25096  uhgrstrrepe  25745  wlkntrllem3  26091  frgrancvvdeqlem4  26560  vc2OLD  26807  nvge0  26912  nmoo0  27030  bcsiALT  27420  pjchi  27675  shjshseli  27736  spanpr  27823  pjinvari  28434  mdslmd1lem2  28569  iundifdifd  28762  iundifdif  28763  gtiso  28861  rngurd  29119  esumpr2  29456  omssubaddlem  29688  eulerpartlemt  29760  ofcccat  29946  topjoin  31530  tailfval  31537  tailf  31540  dvasin  32666  dvacos  32667  opidon2OLD  32823  cdleme4  34543  cdleme22e  34650  cdleme22eALTN  34651  cdleme42a  34777  cdleme42d  34779  cdlemk20  35180  dih1dimatlem0  35635  lcfrlem2  35850  elrfi  36275  fzsplit1nn0  36335  rabdiophlem2  36384  eldioph4b  36393  diophren  36395  pell1qrgaplem  36455  rngunsnply  36762  compne  37665  fmuldfeq  38650  limciccioolb  38688  ditgeq3d  38856  stoweidlem44  38937  dirkertrigeq  38994  fourierdlem32  39032  fourierdlem33  39033  fourierdlem42  39042  fourierdlem62  39061  fourierdlem84  39083  fourierdlem85  39084  fourierdlem97  39096  fourierdlem98  39097  fourierdlem102  39101  fourierdlem104  39103  fourierdlem113  39112  fourierdlem114  39113  fourierswlem  39123  fouriersw  39124  sssalgen  39229  meadjun  39355  deccarry  39941  fpropnf1  40337  fsumsplitsndif  40372  1wlkvtxedg  40852  1wlkres  40879  31wlkond  41338  3cycld  41345  frgrncvvdeqlem4  41472  av-extwwlkfablem1  41508  funcrngcsetcALT  41791