Theorem syl5req 2669

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

Syntax hints:   → wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  syl5reqr  2671  opeqsn  4967  relop  5272  ordintdif  5774  iotanul  5866  funopg  5922  funcnvres  5967  fpropnf1  6524  csbriota  6623  csbov123  6687  mpt2curryd  7395  nneob  7732  sucdom2  8156  unblem2  8213  pwfilem  8260  kmlem2  8973  kmlem11  8982  kmlem12  8983  cflim3  9084  1idsr  9919  recextlem1  10657  quoremz  12654  quoremnn0ALT  12656  intfrac2  12657  hashprg  13182  hashprgOLD  13183  hashfacen  13238  leiso  13243  ccatrid  13370  swrdccat3a  13494  repsw2  13693  repsw3  13694  cvgcmpce  14550  explecnv  14597  risefallfac  14755  ramub1lem1  15730  ressress  15938  subsubc  16513  grp1inv  17523  psgnunilem1  17913  psgn0fv0  17931  psgnsn  17940  efginvrel2  18140  efgredleme  18156  efgcpbllemb  18168  frgpnabllem1  18276  gsumzaddlem  18321  gsumzmhm  18337  fsfnn0gsumfsffz  18379  dprd2da  18441  dpjcntz  18451  dpjdisj  18452  dpjlsm  18453  dpjidcl  18457  ablfac1lem  18467  ablfac1eu  18472  lmhmlsp  19049  mplmon2mul  19501  frlmip  20117  1marepvmarrepid  20381  m1detdiag  20403  cramerimplem2  20490  pmatcollpw3lem  20588  chpscmatgsumbin  20649  chpscmatgsummon  20650  cayhamlem2  20689  neitr  20984  fixufil  21726  trust  22033  restmetu  22375  nmfval2  22395  nmval2  22396  rerest  22607  xrrest  22610  xrge0gsumle  22636  rrxip  23178  voliunlem3  23320  volsup  23324  itg1addlem5  23467  itg2monolem1  23517  itg2cnlem2  23529  itgmpt  23549  iblcnlem1  23554  itgcnlem  23556  itgioo  23582  limcres  23650  mdegfval  23822  dgrlem  23985  coeidlem  23993  mcubic  24574  binom4  24577  dquartlem2  24579  amgm  24717  lgamgulmlem2  24756  eflgam  24771  wilthlem2  24795  rpvmasum2  25201  pntlemo  25296  wlkres  26567  3wlkond  27031  3cycld  27038  frgrncvvdeqlem3  27165  extwwlkfablem1  27207  vc2OLD  27423  nvge0  27528  nmoo0  27646  bcsiALT  28036  pjchi  28291  shjshseli  28352  spanpr  28439  pjinvari  29050  mdslmd1lem2  29185  iundifdifd  29380  iundifdif  29381  fmptco1f1o  29434  gtiso  29478  rngurd  29788  esumpr2  30129  omssubaddlem  30361  eulerpartlemt  30433  ofcccat  30620  topjoin  32360  tailfval  32367  tailf  32370  dvasin  33496  dvacos  33497  opidon2OLD  33653  cdleme4  35525  cdleme22e  35632  cdleme22eALTN  35633  cdleme42a  35759  cdleme42d  35761  cdlemk20  36162  dih1dimatlem0  36617  lcfrlem2  36832  elrfi  37257  fzsplit1nn0  37317  rabdiophlem2  37366  eldioph4b  37375  diophren  37377  pell1qrgaplem  37437  rngunsnply  37743  compneOLD  38644  fmuldfeq  39815  limciccioolb  39853  ditgeq3d  40180  stoweidlem44  40261  dirkertrigeq  40318  fourierdlem32  40356  fourierdlem33  40357  fourierdlem42  40366  fourierdlem62  40385  fourierdlem84  40407  fourierdlem85  40408  fourierdlem97  40420  fourierdlem98  40421  fourierdlem102  40425  fourierdlem104  40427  fourierdlem113  40436  fourierdlem114  40437  fourierswlem  40447  fouriersw  40448  sssalgen  40553  meadjun  40679  deccarry  41321  fsumsplitsndif  41343  funcrngcsetcALT  41999