Theorem eqtr2id 2800

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

Syntax hints:   → wi 4   = wceq 1550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744

This theorem is referenced by:  eqtr3di  2802  opeqsng  5462  relop  5811  ordintdif  6382  iotanul  6486  funopg  6540  funcnvres  6584  fpropnf1  7236  csbriota  7353  csbov123  7425  mpocurryd  8233  om2  8539  nneob  8610  sucdom2  9156  unblem2  9222  pwfilem  9247  prfi  9253  pr2ne  9947  kmlem2  10094  kmlem11  10103  kmlem12  10104  cflim3  10205  1idsr  11042  recextlem1  11803  quoremz  13851  quoremnn0ALT  13853  intfrac2  13854  hashprg  14394  hashfacen  14453  leiso  14458  ccatrid  14587  repsw2  14949  repsw3  14950  cvgcmpce  15818  explecnv  15867  risefallfac  16026  ramub1lem1  17034  ressress  17255  subsubc  17858  chnfi  18638  grp1inv  19062  eqg0subg  19209  psgnunilem1  19505  psgn0fv0  19523  psgnsn  19532  efginvrel2  19739  efgredleme  19755  efgcpbllemb  19767  cmnbascntr  19817  frgpnabllem1  19885  gsumzaddlem  19933  gsumzmhm  19949  fsfnn0gsumfsffz  19995  dprd2da  20056  dpjcntz  20066  dpjdisj  20067  dpjlsm  20068  dpjidcl  20072  ablfac1lem  20082  ablfac1eu  20087  ringurd  20203  funcrngcsetcALT  20659  lmhmlsp  21085  elrspsn  21279  frlmip  21799  opsrtoslem2  22078  mplmon2mul  22091  1marepvmarrepid  22604  m1detdiag  22626  cramerimplem2  22713  pmatcollpw3lem  22812  chpscmatgsumbin  22873  chpscmatgsummon  22874  cayhamlem2  22913  neitr  23209  fixufil  23951  trust  24258  restmetu  24599  nmfval0  24619  nmval2  24621  rerest  24833  xrrest  24837  xrge0gsumle  24863  mpomulcn  24898  rrxip  25421  rrx0  25428  rrxdsfi  25442  voliunlem3  25583  volsup  25587  itg1addlem5  25731  itg2monolem1  25781  itg2cnlem2  25793  itgmpt  25814  iblcnlem1  25819  itgcnlem  25821  itgioo  25847  limcres  25917  mdegfval  26091  dgrlem  26258  coeidlem  26266  mcubic  26878  binom4  26881  dquartlem2  26883  amgm  27021  lgamgulmlem2  27060  eflgam  27075  wilthlem2  27099  rpvmasum2  27542  pntlemo  27637  bday0b  27872  pw2cut2  28521  zz12s  28534  wlkres  29804  3wlkond  30308  3cycld  30315  frgrncvvdeqlem3  30438  vc2OLD  30706  nvge0  30811  nmoo0  30929  bcsiALT  31317  pjchi  31570  shjshseli  31631  spanpr  31718  pjinvari  32329  mdslmd1lem2  32464  iundifdifd  32699  iundifdif  32700  fmptco1f1o  32774  gtiso  32842  gsumhashmul  33197  cycpmco2lem4  33259  cycpmconjslem2  33285  qusima  33540  mxidlirred  33604  selvascl  33758  esplyind  33816  vietalem  33820  extdgfialglem1  33933  2sqr3minply  34021  zarcls0  34109  esumpr2  34308  omssubaddlem  34540  eulerpartlemt  34612  ofcccat  34784  2cycld  35426  satfv1lem  35650  topjoin  36663  tailfval  36670  tailf  36673  dvasin  38141  dvacos  38142  opidon2OLD  38291  cdleme4  40800  cdleme22e  40906  cdleme22eALTN  40907  cdleme42a  41033  cdleme42d  41035  cdlemk20  41436  dih1dimatlem0  41890  lcfrlem2  42105  elrfi  43213  fzsplit1nn0  43273  rabdiophlem2  43317  eldioph4b  43326  diophren  43328  pell1qrgaplem  43388  rngunsnply  43684  oe2  43920  disjinfi  45708  fmuldfeq  46097  limciccioolb  46135  ditgeq3d  46476  stoweidlem44  46556  dirkertrigeq  46613  fourierdlem32  46651  fourierdlem33  46652  fourierdlem42  46661  fourierdlem62  46680  fourierdlem84  46702  fourierdlem85  46703  fourierdlem97  46715  fourierdlem98  46716  fourierdlem102  46720  fourierdlem104  46722  fourierdlem113  46731  fourierdlem114  46732  fourierswlem  46742  fouriersw  46743  sssalgen  46847  meadjun  46974  cos3t  47404  sin5tlem1  47405  fcoreslem2  47596  fnfocofob  47611  deccarry  47843  fsumsplitsndif  47913  gricushgr  48477  ushggricedg  48487  2sphere  49309  iscnrm3rlem1  49499