Theorem eqtr2id 2777

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqtr3di  2779  opeqsng  5450  relop  5797  ordintdif  6362  iotanul  6466  funopg  6520  funcnvres  6564  fpropnf1  7208  csbriota  7325  csbov123  7397  mpocurryd  8209  nneob  8581  sucdom2  9127  unblem2  9198  pwfilem  9225  prfi  9232  pr2ne  9918  kmlem2  10065  kmlem11  10074  kmlem12  10075  cflim3  10175  1idsr  11011  recextlem1  11768  quoremz  13777  quoremnn0ALT  13779  intfrac2  13780  hashprg  14320  hashfacen  14379  leiso  14384  ccatrid  14512  repsw2  14875  repsw3  14876  cvgcmpce  15743  explecnv  15790  risefallfac  15949  ramub1lem1  16956  ressress  17176  subsubc  17778  grp1inv  18945  eqg0subg  19093  psgnunilem1  19390  psgn0fv0  19408  psgnsn  19417  efginvrel2  19624  efgredleme  19640  efgcpbllemb  19652  cmnbascntr  19702  frgpnabllem1  19770  gsumzaddlem  19818  gsumzmhm  19834  fsfnn0gsumfsffz  19880  dprd2da  19941  dpjcntz  19951  dpjdisj  19952  dpjlsm  19953  dpjidcl  19957  ablfac1lem  19967  ablfac1eu  19972  ringurd  20088  funcrngcsetcALT  20544  lmhmlsp  20971  elrspsn  21165  frlmip  21703  opsrtoslem2  21979  mplmon2mul  21992  1marepvmarrepid  22478  m1detdiag  22500  cramerimplem2  22587  pmatcollpw3lem  22686  chpscmatgsumbin  22747  chpscmatgsummon  22748  cayhamlem2  22787  neitr  23083  fixufil  23825  trust  24133  restmetu  24474  nmfval0  24494  nmval2  24496  rerest  24708  xrrest  24712  xrge0gsumle  24738  mpomulcn  24774  rrxip  25306  rrx0  25313  rrxdsfi  25327  voliunlem3  25469  volsup  25473  itg1addlem5  25617  itg2monolem1  25667  itg2cnlem2  25679  itgmpt  25700  iblcnlem1  25705  itgcnlem  25707  itgioo  25733  limcres  25803  mdegfval  25983  dgrlem  26150  coeidlem  26158  mcubic  26773  binom4  26776  dquartlem2  26778  amgm  26917  lgamgulmlem2  26956  eflgam  26971  wilthlem2  26995  rpvmasum2  27439  pntlemo  27534  bday0b  27762  zzs12  28370  wlkres  29632  3wlkond  30133  3cycld  30140  frgrncvvdeqlem3  30263  vc2OLD  30530  nvge0  30635  nmoo0  30753  bcsiALT  31141  pjchi  31394  shjshseli  31455  spanpr  31542  pjinvari  32153  mdslmd1lem2  32288  iundifdifd  32523  iundifdif  32524  fmptco1f1o  32590  gtiso  32657  gsumhashmul  33027  cycpmco2lem4  33084  cycpmconjslem2  33110  qusima  33358  mxidlirred  33422  2sqr3minply  33749  zarcls0  33837  esumpr2  34036  omssubaddlem  34269  eulerpartlemt  34341  ofcccat  34513  2cycld  35113  satfv1lem  35337  topjoin  36341  tailfval  36348  tailf  36351  dvasin  37686  dvacos  37687  opidon2OLD  37836  cdleme4  40220  cdleme22e  40326  cdleme22eALTN  40327  cdleme42a  40453  cdleme42d  40455  cdlemk20  40856  dih1dimatlem0  41310  lcfrlem2  41525  elrfi  42670  fzsplit1nn0  42730  rabdiophlem2  42778  eldioph4b  42787  diophren  42789  pell1qrgaplem  42849  rngunsnply  43145  om2  43380  oe2  43382  disjinfi  45173  fmuldfeq  45568  limciccioolb  45606  ditgeq3d  45949  stoweidlem44  46029  dirkertrigeq  46086  fourierdlem32  46124  fourierdlem33  46125  fourierdlem42  46134  fourierdlem62  46153  fourierdlem84  46175  fourierdlem85  46176  fourierdlem97  46188  fourierdlem98  46189  fourierdlem102  46193  fourierdlem104  46195  fourierdlem113  46204  fourierdlem114  46205  fourierswlem  46215  fouriersw  46216  sssalgen  46320  meadjun  46447  fcoreslem2  47052  fnfocofob  47067  deccarry  47299  fsumsplitsndif  47361  gricushgr  47905  ushggricedg  47915  2sphere  48738  iscnrm3rlem1  48928