Theorem eqtr2id 2813

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

Syntax hints:   → wi 4   = wceq 1563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  eqtr3di  2815  opeqsng  5476  relop  5826  ordintdif  6401  iotanul  6505  funopg  6559  funcnvres  6603  fpropnf1  7255  csbriota  7372  csbov123  7444  mpocurryd  8253  om2  8559  nneob  8630  sucdom2  9175  unblem2  9241  pwfilem  9265  prfi  9271  pr2ne  9977  kmlem2  10123  kmlem11  10132  kmlem12  10133  cflim3  10234  1idsr  11071  recextlem1  11832  quoremz  13876  quoremnn0ALT  13878  intfrac2  13879  hashprg  14419  hashfacen  14479  leiso  14484  ccatrid  14613  repsw2  14975  repsw3  14976  cvgcmpce  15858  explecnv  15907  risefallfac  16066  ramub1lem1  17074  ressress  17295  subsubc  17898  chnfi  18678  grp1inv  19102  eqg0subg  19255  psgnunilem1  19551  psgn0fv0  19569  psgnsn  19578  efginvrel2  19785  efgredleme  19801  efgcpbllemb  19813  cmnbascntr  19863  frgpnabllem1  19931  gsumzaddlem  19979  gsumzmhm  19995  fsfnn0gsumfsffz  20041  dprd2da  20102  dpjcntz  20112  dpjdisj  20113  dpjlsm  20114  dpjidcl  20118  ablfac1lem  20128  ablfac1eu  20133  ringurd  20255  funcrngcsetcALT  20714  lmhmlsp  21136  elrspsn  21335  frlmip  21885  opsrtoslem2  22164  mplmon2mul  22177  1marepvmarrepid  22689  m1detdiag  22711  cramerimplem2  22798  pmatcollpw3lem  22897  chpscmatgsumbin  22958  chpscmatgsummon  22959  cayhamlem2  22998  neitr  23294  fixufil  24036  trust  24343  restmetu  24684  nmfval0  24704  nmval2  24706  rerest  24918  xrrest  24922  xrge0gsumle  24948  mpomulcn  24983  rrxip  25506  rrx0  25513  rrxdsfi  25527  voliunlem3  25668  volsup  25672  itg1addlem5  25816  itg2monolem1  25866  itg2cnlem2  25878  itgmpt  25899  iblcnlem1  25904  itgcnlem  25906  itgioo  25932  limcres  26002  mdegfval  26176  dgrlem  26343  coeidlem  26351  mcubic  26966  binom4  26969  dquartlem2  26971  amgm  27109  lgamgulmlem2  27148  eflgam  27163  wilthlem2  27187  rpvmasum2  27630  pntlemo  27725  bday0b  27960  pw2cut2  28609  zz12s  28622  wlkres  29923  3wlkond  30427  3cycld  30434  frgrncvvdeqlem3  30557  vc2OLD  30825  nvge0  30930  nmoo0  31048  bcsiALT  31436  pjchi  31689  shjshseli  31750  spanpr  31837  pjinvari  32448  mdslmd1lem2  32583  iundifdifd  32812  iundifdif  32813  fresunsn  32878  fmptco1f1o  32886  gtiso  32954  gsumhashmul  33295  cycpmco2lem4  33357  cycpmconjslem2  33383  qusima  33628  mxidlirred  33667  selvascl  33819  esplyind  33877  vietalem  33881  extdgfialglem1  33994  2sqr3minply  34082  zarcls0  34170  esumpr2  34369  omssubaddlem  34601  eulerpartlemt  34673  ofcccat  34845  2cycld  35496  satfv1lem  35720  topjoin  36733  tailfval  36740  tailf  36743  dvasin  38210  dvacos  38211  opidon2OLD  38360  cdleme4  40869  cdleme22e  40975  cdleme22eALTN  40976  cdleme42a  41102  cdleme42d  41104  cdlemk20  41505  dih1dimatlem0  41959  lcfrlem2  42174  elrfi  43282  fzsplit1nn0  43342  rabdiophlem2  43386  eldioph4b  43395  diophren  43397  pell1qrgaplem  43457  rngunsnply  43753  oe2  43989  disjinfi  45769  fmuldfeq  46158  limciccioolb  46196  ditgeq3d  46537  stoweidlem44  46617  dirkertrigeq  46674  fourierdlem32  46712  fourierdlem33  46713  fourierdlem42  46722  fourierdlem62  46741  fourierdlem84  46763  fourierdlem85  46764  fourierdlem97  46776  fourierdlem98  46777  fourierdlem102  46781  fourierdlem104  46783  fourierdlem113  46792  fourierdlem114  46793  fourierswlem  46803  fouriersw  46804  sssalgen  46908  meadjun  47035  cos3t  47465  sin5tlem1  47466  fcoreslem2  47657  fnfocofob  47672  deccarry  47904  fsumsplitsndif  47974  gricushgr  48538  ushggricedg  48548  2sphere  49381  iscnrm3rlem1  49570