Theorem eqtr2id 2783

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 2782	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2741	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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqtr3di  2785  opeqsng  5478  relop  5830  ordintdif  6403  iotanul  6509  funopg  6570  funcnvres  6614  fpropnf1  7260  csbriota  7377  csbov123  7449  mpocurryd  8268  nneob  8668  sucdom2OLD  9096  sucdom2  9217  unblem2  9301  pwfilem  9328  prfi  9335  pr2ne  10018  kmlem2  10166  kmlem11  10175  kmlem12  10176  cflim3  10276  1idsr  11112  recextlem1  11867  quoremz  13872  quoremnn0ALT  13874  intfrac2  13875  hashprg  14413  hashfacen  14472  leiso  14477  ccatrid  14605  repsw2  14969  repsw3  14970  cvgcmpce  15834  explecnv  15881  risefallfac  16040  ramub1lem1  17046  ressress  17268  subsubc  17866  grp1inv  19031  eqg0subg  19179  psgnunilem1  19474  psgn0fv0  19492  psgnsn  19501  efginvrel2  19708  efgredleme  19724  efgcpbllemb  19736  cmnbascntr  19786  frgpnabllem1  19854  gsumzaddlem  19902  gsumzmhm  19918  fsfnn0gsumfsffz  19964  dprd2da  20025  dpjcntz  20035  dpjdisj  20036  dpjlsm  20037  dpjidcl  20041  ablfac1lem  20051  ablfac1eu  20056  ringurd  20145  funcrngcsetcALT  20601  lmhmlsp  21007  elrspsn  21201  frlmip  21738  opsrtoslem2  22014  mplmon2mul  22027  1marepvmarrepid  22513  m1detdiag  22535  cramerimplem2  22622  pmatcollpw3lem  22721  chpscmatgsumbin  22782  chpscmatgsummon  22783  cayhamlem2  22822  neitr  23118  fixufil  23860  trust  24168  restmetu  24509  nmfval0  24529  nmval2  24531  rerest  24743  xrrest  24747  xrge0gsumle  24773  mpomulcn  24809  rrxip  25342  rrx0  25349  rrxdsfi  25363  voliunlem3  25505  volsup  25509  itg1addlem5  25653  itg2monolem1  25703  itg2cnlem2  25715  itgmpt  25736  iblcnlem1  25741  itgcnlem  25743  itgioo  25769  limcres  25839  mdegfval  26019  dgrlem  26186  coeidlem  26194  mcubic  26809  binom4  26812  dquartlem2  26814  amgm  26953  lgamgulmlem2  26992  eflgam  27007  wilthlem2  27031  rpvmasum2  27475  pntlemo  27570  bday0b  27794  zzs12  28391  wlkres  29650  3wlkond  30152  3cycld  30159  frgrncvvdeqlem3  30282  vc2OLD  30549  nvge0  30654  nmoo0  30772  bcsiALT  31160  pjchi  31413  shjshseli  31474  spanpr  31561  pjinvari  32172  mdslmd1lem2  32307  iundifdifd  32542  iundifdif  32543  fmptco1f1o  32611  gtiso  32678  gsumhashmul  33055  cycpmco2lem4  33140  cycpmconjslem2  33166  qusima  33423  mxidlirred  33487  2sqr3minply  33814  zarcls0  33899  esumpr2  34098  omssubaddlem  34331  eulerpartlemt  34403  ofcccat  34575  2cycld  35160  satfv1lem  35384  topjoin  36383  tailfval  36390  tailf  36393  dvasin  37728  dvacos  37729  opidon2OLD  37878  cdleme4  40257  cdleme22e  40363  cdleme22eALTN  40364  cdleme42a  40490  cdleme42d  40492  cdlemk20  40893  dih1dimatlem0  41347  lcfrlem2  41562  elrfi  42717  fzsplit1nn0  42777  rabdiophlem2  42825  eldioph4b  42834  diophren  42836  pell1qrgaplem  42896  rngunsnply  43193  om2  43428  oe2  43430  disjinfi  45216  fmuldfeq  45612  limciccioolb  45650  ditgeq3d  45993  stoweidlem44  46073  dirkertrigeq  46130  fourierdlem32  46168  fourierdlem33  46169  fourierdlem42  46178  fourierdlem62  46197  fourierdlem84  46219  fourierdlem85  46220  fourierdlem97  46232  fourierdlem98  46233  fourierdlem102  46237  fourierdlem104  46239  fourierdlem113  46248  fourierdlem114  46249  fourierswlem  46259  fouriersw  46260  sssalgen  46364  meadjun  46491  fcoreslem2  47093  fnfocofob  47108  deccarry  47340  fsumsplitsndif  47387  gricushgr  47930  ushggricedg  47940  2sphere  48729  iscnrm3rlem1  48914