Theorem eqtr2id 2784

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

Hypotheses

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

Assertion

Ref	Expression
eqtr2id	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2id

Step	Hyp	Ref	Expression
1		eqtr2id.1	. . 3 ⊢ 𝐴 = 𝐵
2		eqtr2id.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	syl5eq 2783	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2742	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  eqtr3di  2786  opeqsng  5371  relop  5704  ordintdif  6240  iotanul  6336  funopg  6392  funcnvres  6436  fpropnf1  7057  csbriota  7164  csbov123  7233  mpocurryd  7989  nneob  8359  sucdom2  8733  pwfilem  8832  unblem2  8902  pwfilemOLD  8948  kmlem2  9730  kmlem11  9739  kmlem12  9740  cflim3  9841  1idsr  10677  recextlem1  11427  quoremz  13393  quoremnn0ALT  13395  intfrac2  13396  hashprg  13927  hashfacen  13983  hashfacenOLD  13984  leiso  13990  ccatrid  14109  repsw2  14480  repsw3  14481  cvgcmpce  15345  explecnv  15392  risefallfac  15549  ramub1lem1  16542  ressress  16746  subsubc  17313  grp1inv  18425  psgnunilem1  18839  psgn0fv0  18857  psgnsn  18866  efginvrel2  19071  efgredleme  19087  efgcpbllemb  19099  frgpnabllem1  19212  gsumzaddlem  19260  gsumzmhm  19276  fsfnn0gsumfsffz  19322  dprd2da  19383  dpjcntz  19393  dpjdisj  19394  dpjlsm  19395  dpjidcl  19399  ablfac1lem  19409  ablfac1eu  19414  rnrhmsubrg  19786  lmhmlsp  20040  frlmip  20694  mplmon2mul  20981  1marepvmarrepid  21426  m1detdiag  21448  cramerimplem2  21535  pmatcollpw3lem  21634  chpscmatgsumbin  21695  chpscmatgsummon  21696  cayhamlem2  21735  neitr  22031  fixufil  22773  trust  23081  restmetu  23422  nmfval0  23442  nmval2  23444  rerest  23655  xrrest  23658  xrge0gsumle  23684  rrxip  24241  rrx0  24248  rrxdsfi  24262  voliunlem3  24403  volsup  24407  itg1addlem5  24552  itg2monolem1  24602  itg2cnlem2  24614  itgmpt  24634  iblcnlem1  24639  itgcnlem  24641  itgioo  24667  limcres  24737  mdegfval  24914  dgrlem  25077  coeidlem  25085  mcubic  25684  binom4  25687  dquartlem2  25689  amgm  25827  lgamgulmlem2  25866  eflgam  25881  wilthlem2  25905  rpvmasum2  26347  pntlemo  26442  wlkres  27712  3wlkond  28208  3cycld  28215  frgrncvvdeqlem3  28338  vc2OLD  28603  nvge0  28708  nmoo0  28826  bcsiALT  29214  pjchi  29467  shjshseli  29528  spanpr  29615  pjinvari  30226  mdslmd1lem2  30361  iundifdifd  30574  iundifdif  30575  fmptco1f1o  30641  gtiso  30707  gsumhashmul  30989  cycpmco2lem4  31069  cycpmconjslem2  31095  rngurd  31155  rspsnel  31235  qusima  31262  zarcls0  31486  esumpr2  31701  omssubaddlem  31932  eulerpartlemt  32004  ofcccat  32188  2cycld  32767  satfv1lem  32991  bday0b  33710  topjoin  34240  tailfval  34247  tailf  34250  dvasin  35547  dvacos  35548  opidon2OLD  35698  cdleme4  37938  cdleme22e  38044  cdleme22eALTN  38045  cdleme42a  38171  cdleme42d  38173  cdlemk20  38574  dih1dimatlem0  39028  lcfrlem2  39243  elrfi  40160  fzsplit1nn0  40220  rabdiophlem2  40268  eldioph4b  40277  diophren  40279  pell1qrgaplem  40339  rngunsnply  40642  disjinfi  42345  fmuldfeq  42742  limciccioolb  42780  ditgeq3d  43123  stoweidlem44  43203  dirkertrigeq  43260  fourierdlem32  43298  fourierdlem33  43299  fourierdlem42  43308  fourierdlem62  43327  fourierdlem84  43349  fourierdlem85  43350  fourierdlem97  43362  fourierdlem98  43363  fourierdlem102  43367  fourierdlem104  43369  fourierdlem113  43378  fourierdlem114  43379  fourierswlem  43389  fouriersw  43390  sssalgen  43492  meadjun  43618  fcoreslem2  44173  fnfocofob  44186  deccarry  44419  fsumsplitsndif  44441  isomushgr  44894  ushrisomgr  44909  funcrngcsetcALT  45173  2sphere  45711  iscnrm3rlem1  45850