Theorem eqtr2id 2785

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqtr3di  2787  opeqsng  5459  relop  5807  ordintdif  6376  iotanul  6480  funopg  6534  funcnvres  6578  fpropnf1  7223  csbriota  7340  csbov123  7412  mpocurryd  8221  om2  8523  nneob  8594  sucdom2  9139  unblem2  9205  pwfilem  9230  prfi  9236  pr2ne  9927  kmlem2  10074  kmlem11  10083  kmlem12  10084  cflim3  10184  1idsr  11021  recextlem1  11779  quoremz  13787  quoremnn0ALT  13789  intfrac2  13790  hashprg  14330  hashfacen  14389  leiso  14394  ccatrid  14523  repsw2  14885  repsw3  14886  cvgcmpce  15753  explecnv  15800  risefallfac  15959  ramub1lem1  16966  ressress  17186  subsubc  17789  chnfi  18569  grp1inv  18990  eqg0subg  19137  psgnunilem1  19434  psgn0fv0  19452  psgnsn  19461  efginvrel2  19668  efgredleme  19684  efgcpbllemb  19696  cmnbascntr  19746  frgpnabllem1  19814  gsumzaddlem  19862  gsumzmhm  19878  fsfnn0gsumfsffz  19924  dprd2da  19985  dpjcntz  19995  dpjdisj  19996  dpjlsm  19997  dpjidcl  20001  ablfac1lem  20011  ablfac1eu  20016  ringurd  20132  funcrngcsetcALT  20586  lmhmlsp  21013  elrspsn  21207  frlmip  21745  opsrtoslem2  22023  mplmon2mul  22036  1marepvmarrepid  22531  m1detdiag  22553  cramerimplem2  22640  pmatcollpw3lem  22739  chpscmatgsumbin  22800  chpscmatgsummon  22801  cayhamlem2  22840  neitr  23136  fixufil  23878  trust  24185  restmetu  24526  nmfval0  24546  nmval2  24548  rerest  24760  xrrest  24764  xrge0gsumle  24790  mpomulcn  24826  rrxip  25358  rrx0  25365  rrxdsfi  25379  voliunlem3  25521  volsup  25525  itg1addlem5  25669  itg2monolem1  25719  itg2cnlem2  25731  itgmpt  25752  iblcnlem1  25757  itgcnlem  25759  itgioo  25785  limcres  25855  mdegfval  26035  dgrlem  26202  coeidlem  26210  mcubic  26825  binom4  26828  dquartlem2  26830  amgm  26969  lgamgulmlem2  27008  eflgam  27023  wilthlem2  27047  rpvmasum2  27491  pntlemo  27586  bday0b  27821  pw2cut2  28470  zz12s  28483  wlkres  29754  3wlkond  30258  3cycld  30265  frgrncvvdeqlem3  30388  vc2OLD  30655  nvge0  30760  nmoo0  30878  bcsiALT  31266  pjchi  31519  shjshseli  31580  spanpr  31667  pjinvari  32278  mdslmd1lem2  32413  iundifdifd  32647  iundifdif  32648  fmptco1f1o  32722  gtiso  32790  gsumhashmul  33160  cycpmco2lem4  33222  cycpmconjslem2  33248  qusima  33500  mxidlirred  33564  esplyind  33751  vietalem  33755  extdgfialglem1  33869  2sqr3minply  33957  zarcls0  34045  esumpr2  34244  omssubaddlem  34476  eulerpartlemt  34548  ofcccat  34720  2cycld  35351  satfv1lem  35575  topjoin  36578  tailfval  36585  tailf  36588  dvasin  37952  dvacos  37953  opidon2OLD  38102  cdleme4  40611  cdleme22e  40717  cdleme22eALTN  40718  cdleme42a  40844  cdleme42d  40846  cdlemk20  41247  dih1dimatlem0  41701  lcfrlem2  41916  elrfi  43048  fzsplit1nn0  43108  rabdiophlem2  43156  eldioph4b  43165  diophren  43167  pell1qrgaplem  43227  rngunsnply  43523  oe2  43759  disjinfi  45548  fmuldfeq  45940  limciccioolb  45978  ditgeq3d  46319  stoweidlem44  46399  dirkertrigeq  46456  fourierdlem32  46494  fourierdlem33  46495  fourierdlem42  46504  fourierdlem62  46523  fourierdlem84  46545  fourierdlem85  46546  fourierdlem97  46558  fourierdlem98  46559  fourierdlem102  46563  fourierdlem104  46565  fourierdlem113  46574  fourierdlem114  46575  fourierswlem  46585  fouriersw  46586  sssalgen  46690  meadjun  46817  fcoreslem2  47421  fnfocofob  47436  deccarry  47668  fsumsplitsndif  47730  gricushgr  48274  ushggricedg  48284  2sphere  49106  iscnrm3rlem1  49296