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  5451  relop  5799  ordintdif  6368  iotanul  6472  funopg  6526  funcnvres  6570  fpropnf1  7215  csbriota  7332  csbov123  7404  mpocurryd  8212  om2  8514  nneob  8585  sucdom2  9130  unblem2  9196  pwfilem  9221  prfi  9227  pr2ne  9918  kmlem2  10065  kmlem11  10074  kmlem12  10075  cflim3  10175  1idsr  11012  recextlem1  11771  quoremz  13805  quoremnn0ALT  13807  intfrac2  13808  hashprg  14348  hashfacen  14407  leiso  14412  ccatrid  14541  repsw2  14903  repsw3  14904  cvgcmpce  15772  explecnv  15821  risefallfac  15980  ramub1lem1  16988  ressress  17208  subsubc  17811  chnfi  18591  grp1inv  19015  eqg0subg  19162  psgnunilem1  19459  psgn0fv0  19477  psgnsn  19486  efginvrel2  19693  efgredleme  19709  efgcpbllemb  19721  cmnbascntr  19771  frgpnabllem1  19839  gsumzaddlem  19887  gsumzmhm  19903  fsfnn0gsumfsffz  19949  dprd2da  20010  dpjcntz  20020  dpjdisj  20021  dpjlsm  20022  dpjidcl  20026  ablfac1lem  20036  ablfac1eu  20041  ringurd  20157  funcrngcsetcALT  20609  lmhmlsp  21036  elrspsn  21230  frlmip  21768  opsrtoslem2  22044  mplmon2mul  22057  1marepvmarrepid  22550  m1detdiag  22572  cramerimplem2  22659  pmatcollpw3lem  22758  chpscmatgsumbin  22819  chpscmatgsummon  22820  cayhamlem2  22859  neitr  23155  fixufil  23897  trust  24204  restmetu  24545  nmfval0  24565  nmval2  24567  rerest  24779  xrrest  24783  xrge0gsumle  24809  mpomulcn  24844  rrxip  25367  rrx0  25374  rrxdsfi  25388  voliunlem3  25529  volsup  25533  itg1addlem5  25677  itg2monolem1  25727  itg2cnlem2  25739  itgmpt  25760  iblcnlem1  25765  itgcnlem  25767  itgioo  25793  limcres  25863  mdegfval  26037  dgrlem  26204  coeidlem  26212  mcubic  26824  binom4  26827  dquartlem2  26829  amgm  26968  lgamgulmlem2  27007  eflgam  27022  wilthlem2  27046  rpvmasum2  27489  pntlemo  27584  bday0b  27819  pw2cut2  28468  zz12s  28481  wlkres  29752  3wlkond  30256  3cycld  30263  frgrncvvdeqlem3  30386  vc2OLD  30654  nvge0  30759  nmoo0  30877  bcsiALT  31265  pjchi  31518  shjshseli  31579  spanpr  31666  pjinvari  32277  mdslmd1lem2  32412  iundifdifd  32646  iundifdif  32647  fmptco1f1o  32721  gtiso  32789  gsumhashmul  33143  cycpmco2lem4  33205  cycpmconjslem2  33231  qusima  33483  mxidlirred  33547  esplyind  33734  vietalem  33738  extdgfialglem1  33852  2sqr3minply  33940  zarcls0  34028  esumpr2  34227  omssubaddlem  34459  eulerpartlemt  34531  ofcccat  34703  2cycld  35336  satfv1lem  35560  topjoin  36563  tailfval  36570  tailf  36573  dvasin  38039  dvacos  38040  opidon2OLD  38189  cdleme4  40698  cdleme22e  40804  cdleme22eALTN  40805  cdleme42a  40931  cdleme42d  40933  cdlemk20  41334  dih1dimatlem0  41788  lcfrlem2  42003  elrfi  43140  fzsplit1nn0  43200  rabdiophlem2  43248  eldioph4b  43257  diophren  43259  pell1qrgaplem  43319  rngunsnply  43615  oe2  43851  disjinfi  45640  fmuldfeq  46031  limciccioolb  46069  ditgeq3d  46410  stoweidlem44  46490  dirkertrigeq  46547  fourierdlem32  46585  fourierdlem33  46586  fourierdlem42  46595  fourierdlem62  46614  fourierdlem84  46636  fourierdlem85  46637  fourierdlem97  46649  fourierdlem98  46650  fourierdlem102  46654  fourierdlem104  46656  fourierdlem113  46665  fourierdlem114  46666  fourierswlem  46676  fouriersw  46677  sssalgen  46781  meadjun  46908  cos3t  47336  sin5tlem1  47337  fcoreslem2  47524  fnfocofob  47539  deccarry  47771  fsumsplitsndif  47841  gricushgr  48405  ushggricedg  48415  2sphere  49237  iscnrm3rlem1  49427