Theorem eqtr2id 2787

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  eqtr3di  2789  opeqsng  5512  relop  5863  ordintdif  6435  iotanul  6540  funopg  6601  funcnvres  6645  fpropnf1  7286  csbriota  7402  csbov123  7474  mpocurryd  8292  nneob  8692  sucdom2OLD  9120  sucdom2  9240  unblem2  9326  pwfilem  9353  prfi  9360  pr2ne  10041  kmlem2  10189  kmlem11  10198  kmlem12  10199  cflim3  10299  1idsr  11135  recextlem1  11890  quoremz  13891  quoremnn0ALT  13893  intfrac2  13894  hashprg  14430  hashfacen  14489  leiso  14494  ccatrid  14621  repsw2  14985  repsw3  14986  cvgcmpce  15850  explecnv  15897  risefallfac  16056  ramub1lem1  17059  ressress  17293  subsubc  17903  grp1inv  19078  eqg0subg  19226  psgnunilem1  19525  psgn0fv0  19543  psgnsn  19552  efginvrel2  19759  efgredleme  19775  efgcpbllemb  19787  cmnbascntr  19837  frgpnabllem1  19905  gsumzaddlem  19953  gsumzmhm  19969  fsfnn0gsumfsffz  20015  dprd2da  20076  dpjcntz  20086  dpjdisj  20087  dpjlsm  20088  dpjidcl  20092  ablfac1lem  20102  ablfac1eu  20107  ringurd  20202  funcrngcsetcALT  20657  lmhmlsp  21065  elrspsn  21267  frlmip  21815  opsrtoslem2  22097  mplmon2mul  22110  1marepvmarrepid  22596  m1detdiag  22618  cramerimplem2  22705  pmatcollpw3lem  22804  chpscmatgsumbin  22865  chpscmatgsummon  22866  cayhamlem2  22905  neitr  23203  fixufil  23945  trust  24253  restmetu  24598  nmfval0  24618  nmval2  24620  rerest  24839  xrrest  24842  xrge0gsumle  24868  mpomulcn  24904  rrxip  25437  rrx0  25444  rrxdsfi  25458  voliunlem3  25600  volsup  25604  itg1addlem5  25749  itg2monolem1  25799  itg2cnlem2  25811  itgmpt  25832  iblcnlem1  25837  itgcnlem  25839  itgioo  25865  limcres  25935  mdegfval  26115  dgrlem  26282  coeidlem  26290  mcubic  26904  binom4  26907  dquartlem2  26909  amgm  27048  lgamgulmlem2  27087  eflgam  27102  wilthlem2  27126  rpvmasum2  27570  pntlemo  27665  bday0b  27889  zzs12  28437  wlkres  29702  3wlkond  30199  3cycld  30206  frgrncvvdeqlem3  30329  vc2OLD  30596  nvge0  30701  nmoo0  30819  bcsiALT  31207  pjchi  31460  shjshseli  31521  spanpr  31608  pjinvari  32219  mdslmd1lem2  32354  iundifdifd  32581  iundifdif  32582  fmptco1f1o  32649  gtiso  32715  gsumhashmul  33046  cycpmco2lem4  33131  cycpmconjslem2  33157  qusima  33415  mxidlirred  33479  2sqr3minply  33752  zarcls0  33828  esumpr2  34047  omssubaddlem  34280  eulerpartlemt  34352  ofcccat  34536  2cycld  35122  satfv1lem  35346  topjoin  36347  tailfval  36354  tailf  36357  dvasin  37690  dvacos  37691  opidon2OLD  37840  cdleme4  40220  cdleme22e  40326  cdleme22eALTN  40327  cdleme42a  40453  cdleme42d  40455  cdlemk20  40856  dih1dimatlem0  41310  lcfrlem2  41525  elrfi  42681  fzsplit1nn0  42741  rabdiophlem2  42789  eldioph4b  42798  diophren  42800  pell1qrgaplem  42860  rngunsnply  43157  om2  43393  oe2  43395  disjinfi  45134  fmuldfeq  45538  limciccioolb  45576  ditgeq3d  45919  stoweidlem44  45999  dirkertrigeq  46056  fourierdlem32  46094  fourierdlem33  46095  fourierdlem42  46104  fourierdlem62  46123  fourierdlem84  46145  fourierdlem85  46146  fourierdlem97  46158  fourierdlem98  46159  fourierdlem102  46163  fourierdlem104  46165  fourierdlem113  46174  fourierdlem114  46175  fourierswlem  46185  fouriersw  46186  sssalgen  46290  meadjun  46417  fcoreslem2  47013  fnfocofob  47028  deccarry  47260  fsumsplitsndif  47297  gricushgr  47823  ushggricedg  47833  2sphere  48598  iscnrm3rlem1  48736