Theorem eqtr2id 2784

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 2783	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2742	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqtr3di  2786  opeqsng  5451  relop  5799  ordintdif  6368  iotanul  6472  funopg  6526  funcnvres  6570  fpropnf1  7213  csbriota  7330  csbov123  7402  mpocurryd  8211  om2  8513  nneob  8584  sucdom2  9127  unblem2  9193  pwfilem  9218  prfi  9224  pr2ne  9915  kmlem2  10062  kmlem11  10071  kmlem12  10072  cflim3  10172  1idsr  11009  recextlem1  11767  quoremz  13775  quoremnn0ALT  13777  intfrac2  13778  hashprg  14318  hashfacen  14377  leiso  14382  ccatrid  14511  repsw2  14873  repsw3  14874  cvgcmpce  15741  explecnv  15788  risefallfac  15947  ramub1lem1  16954  ressress  17174  subsubc  17777  chnfi  18557  grp1inv  18978  eqg0subg  19125  psgnunilem1  19422  psgn0fv0  19440  psgnsn  19449  efginvrel2  19656  efgredleme  19672  efgcpbllemb  19684  cmnbascntr  19734  frgpnabllem1  19802  gsumzaddlem  19850  gsumzmhm  19866  fsfnn0gsumfsffz  19912  dprd2da  19973  dpjcntz  19983  dpjdisj  19984  dpjlsm  19985  dpjidcl  19989  ablfac1lem  19999  ablfac1eu  20004  ringurd  20120  funcrngcsetcALT  20574  lmhmlsp  21001  elrspsn  21195  frlmip  21733  opsrtoslem2  22011  mplmon2mul  22024  1marepvmarrepid  22519  m1detdiag  22541  cramerimplem2  22628  pmatcollpw3lem  22727  chpscmatgsumbin  22788  chpscmatgsummon  22789  cayhamlem2  22828  neitr  23124  fixufil  23866  trust  24173  restmetu  24514  nmfval0  24534  nmval2  24536  rerest  24748  xrrest  24752  xrge0gsumle  24778  mpomulcn  24814  rrxip  25346  rrx0  25353  rrxdsfi  25367  voliunlem3  25509  volsup  25513  itg1addlem5  25657  itg2monolem1  25707  itg2cnlem2  25719  itgmpt  25740  iblcnlem1  25745  itgcnlem  25747  itgioo  25773  limcres  25843  mdegfval  26023  dgrlem  26190  coeidlem  26198  mcubic  26813  binom4  26816  dquartlem2  26818  amgm  26957  lgamgulmlem2  26996  eflgam  27011  wilthlem2  27035  rpvmasum2  27479  pntlemo  27574  bday0b  27809  pw2cut2  28458  zz12s  28471  wlkres  29742  3wlkond  30246  3cycld  30253  frgrncvvdeqlem3  30376  vc2OLD  30643  nvge0  30748  nmoo0  30866  bcsiALT  31254  pjchi  31507  shjshseli  31568  spanpr  31655  pjinvari  32266  mdslmd1lem2  32401  iundifdifd  32636  iundifdif  32637  fmptco1f1o  32711  gtiso  32780  gsumhashmul  33150  cycpmco2lem4  33211  cycpmconjslem2  33237  qusima  33489  mxidlirred  33553  esplyind  33731  vietalem  33735  extdgfialglem1  33849  2sqr3minply  33937  zarcls0  34025  esumpr2  34224  omssubaddlem  34456  eulerpartlemt  34528  ofcccat  34700  2cycld  35332  satfv1lem  35556  topjoin  36559  tailfval  36566  tailf  36569  dvasin  37905  dvacos  37906  opidon2OLD  38055  cdleme4  40498  cdleme22e  40604  cdleme22eALTN  40605  cdleme42a  40731  cdleme42d  40733  cdlemk20  41134  dih1dimatlem0  41588  lcfrlem2  41803  elrfi  42936  fzsplit1nn0  42996  rabdiophlem2  43044  eldioph4b  43053  diophren  43055  pell1qrgaplem  43115  rngunsnply  43411  oe2  43647  disjinfi  45436  fmuldfeq  45829  limciccioolb  45867  ditgeq3d  46208  stoweidlem44  46288  dirkertrigeq  46345  fourierdlem32  46383  fourierdlem33  46384  fourierdlem42  46393  fourierdlem62  46412  fourierdlem84  46434  fourierdlem85  46435  fourierdlem97  46447  fourierdlem98  46448  fourierdlem102  46452  fourierdlem104  46454  fourierdlem113  46463  fourierdlem114  46464  fourierswlem  46474  fouriersw  46475  sssalgen  46579  meadjun  46706  fcoreslem2  47310  fnfocofob  47325  deccarry  47557  fsumsplitsndif  47619  gricushgr  48163  ushggricedg  48173  2sphere  48995  iscnrm3rlem1  49185