Theorem eqtr2id 2785

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

Syntax hints:   → wi 4   = wceq 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqtr3di  2787  opeqsng  5503  relop  5850  ordintdif  6414  iotanul  6521  funopg  6582  funcnvres  6626  fpropnf1  7265  csbriota  7380  csbov123  7450  mpocurryd  8253  nneob  8654  sucdom2OLD  9081  pwfilem  9176  sucdom2  9205  unblem2  9295  pwfilemOLD  9345  pr2ne  9998  kmlem2  10145  kmlem11  10154  kmlem12  10155  cflim3  10256  1idsr  11092  recextlem1  11843  quoremz  13819  quoremnn0ALT  13821  intfrac2  13822  hashprg  14354  hashfacen  14412  hashfacenOLD  14413  leiso  14419  ccatrid  14536  repsw2  14900  repsw3  14901  cvgcmpce  15763  explecnv  15810  risefallfac  15967  ramub1lem1  16958  ressress  17192  subsubc  17802  grp1inv  18930  eqg0subg  19072  psgnunilem1  19360  psgn0fv0  19378  psgnsn  19387  efginvrel2  19594  efgredleme  19610  efgcpbllemb  19622  cmnbascntr  19672  frgpnabllem1  19740  gsumzaddlem  19788  gsumzmhm  19804  fsfnn0gsumfsffz  19850  dprd2da  19911  dpjcntz  19921  dpjdisj  19922  dpjlsm  19923  dpjidcl  19927  ablfac1lem  19937  ablfac1eu  19942  ringurd  20007  rnrhmsubrg  20351  lmhmlsp  20659  frlmip  21332  mplmon2mul  21629  1marepvmarrepid  22076  m1detdiag  22098  cramerimplem2  22185  pmatcollpw3lem  22284  chpscmatgsumbin  22345  chpscmatgsummon  22346  cayhamlem2  22385  neitr  22683  fixufil  23425  trust  23733  restmetu  24078  nmfval0  24098  nmval2  24100  rerest  24319  xrrest  24322  xrge0gsumle  24348  rrxip  24906  rrx0  24913  rrxdsfi  24927  voliunlem3  25068  volsup  25072  itg1addlem5  25217  itg2monolem1  25267  itg2cnlem2  25279  itgmpt  25299  iblcnlem1  25304  itgcnlem  25306  itgioo  25332  limcres  25402  mdegfval  25579  dgrlem  25742  coeidlem  25750  mcubic  26349  binom4  26352  dquartlem2  26354  amgm  26492  lgamgulmlem2  26531  eflgam  26546  wilthlem2  26570  rpvmasum2  27012  pntlemo  27107  bday0b  27328  wlkres  28924  3wlkond  29421  3cycld  29428  frgrncvvdeqlem3  29551  vc2OLD  29816  nvge0  29921  nmoo0  30039  bcsiALT  30427  pjchi  30680  shjshseli  30741  spanpr  30828  pjinvari  31439  mdslmd1lem2  31574  iundifdifd  31788  iundifdif  31789  fmptco1f1o  31852  gtiso  31917  gsumhashmul  32203  cycpmco2lem4  32283  cycpmconjslem2  32309  rspsnel  32479  qusima  32514  mxidlirred  32583  zarcls0  32843  esumpr2  33060  omssubaddlem  33293  eulerpartlemt  33365  ofcccat  33549  2cycld  34124  satfv1lem  34348  mpomulcn  35157  topjoin  35245  tailfval  35252  tailf  35255  dvasin  36567  dvacos  36568  opidon2OLD  36717  cdleme4  39104  cdleme22e  39210  cdleme22eALTN  39211  cdleme42a  39337  cdleme42d  39339  cdlemk20  39740  dih1dimatlem0  40194  lcfrlem2  40409  elrfi  41422  fzsplit1nn0  41482  rabdiophlem2  41530  eldioph4b  41539  diophren  41541  pell1qrgaplem  41601  rngunsnply  41905  om2  42145  oe2  42147  disjinfi  43881  fmuldfeq  44289  limciccioolb  44327  ditgeq3d  44670  stoweidlem44  44750  dirkertrigeq  44807  fourierdlem32  44845  fourierdlem33  44846  fourierdlem42  44855  fourierdlem62  44874  fourierdlem84  44896  fourierdlem85  44897  fourierdlem97  44909  fourierdlem98  44910  fourierdlem102  44914  fourierdlem104  44916  fourierdlem113  44925  fourierdlem114  44926  fourierswlem  44936  fouriersw  44937  sssalgen  45041  meadjun  45168  fcoreslem2  45764  fnfocofob  45777  deccarry  46009  fsumsplitsndif  46031  isomushgr  46484  ushrisomgr  46499  funcrngcsetcALT  46887  2sphere  47425  iscnrm3rlem1  47563