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 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 2708

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

This theorem is referenced by:  eqtr3di  2786  opeqsng  5457  relop  5805  ordintdif  6374  iotanul  6478  funopg  6532  funcnvres  6576  fpropnf1  7222  csbriota  7339  csbov123  7411  mpocurryd  8219  om2  8521  nneob  8592  sucdom2  9137  unblem2  9203  pwfilem  9228  prfi  9234  pr2ne  9927  kmlem2  10074  kmlem11  10083  kmlem12  10084  cflim3  10184  1idsr  11021  recextlem1  11780  quoremz  13814  quoremnn0ALT  13816  intfrac2  13817  hashprg  14357  hashfacen  14416  leiso  14421  ccatrid  14550  repsw2  14912  repsw3  14913  cvgcmpce  15781  explecnv  15830  risefallfac  15989  ramub1lem1  16997  ressress  17217  subsubc  17820  chnfi  18600  grp1inv  19024  eqg0subg  19171  psgnunilem1  19468  psgn0fv0  19486  psgnsn  19495  efginvrel2  19702  efgredleme  19718  efgcpbllemb  19730  cmnbascntr  19780  frgpnabllem1  19848  gsumzaddlem  19896  gsumzmhm  19912  fsfnn0gsumfsffz  19958  dprd2da  20019  dpjcntz  20029  dpjdisj  20030  dpjlsm  20031  dpjidcl  20035  ablfac1lem  20045  ablfac1eu  20050  ringurd  20166  funcrngcsetcALT  20618  lmhmlsp  21044  elrspsn  21238  frlmip  21758  opsrtoslem2  22034  mplmon2mul  22047  1marepvmarrepid  22540  m1detdiag  22562  cramerimplem2  22649  pmatcollpw3lem  22748  chpscmatgsumbin  22809  chpscmatgsummon  22810  cayhamlem2  22849  neitr  23145  fixufil  23887  trust  24194  restmetu  24535  nmfval0  24555  nmval2  24557  rerest  24769  xrrest  24773  xrge0gsumle  24799  mpomulcn  24834  rrxip  25357  rrx0  25364  rrxdsfi  25378  voliunlem3  25519  volsup  25523  itg1addlem5  25667  itg2monolem1  25717  itg2cnlem2  25729  itgmpt  25750  iblcnlem1  25755  itgcnlem  25757  itgioo  25783  limcres  25853  mdegfval  26027  dgrlem  26194  coeidlem  26202  mcubic  26811  binom4  26814  dquartlem2  26816  amgm  26954  lgamgulmlem2  26993  eflgam  27008  wilthlem2  27032  rpvmasum2  27475  pntlemo  27570  bday0b  27805  pw2cut2  28454  zz12s  28467  wlkres  29737  3wlkond  30241  3cycld  30248  frgrncvvdeqlem3  30371  vc2OLD  30639  nvge0  30744  nmoo0  30862  bcsiALT  31250  pjchi  31503  shjshseli  31564  spanpr  31651  pjinvari  32262  mdslmd1lem2  32397  iundifdifd  32631  iundifdif  32632  fmptco1f1o  32706  gtiso  32774  gsumhashmul  33128  cycpmco2lem4  33190  cycpmconjslem2  33216  qusima  33468  mxidlirred  33532  esplyind  33719  vietalem  33723  extdgfialglem1  33836  2sqr3minply  33924  zarcls0  34012  esumpr2  34211  omssubaddlem  34443  eulerpartlemt  34515  ofcccat  34687  2cycld  35320  satfv1lem  35544  topjoin  36547  tailfval  36554  tailf  36557  dvasin  38025  dvacos  38026  opidon2OLD  38175  cdleme4  40684  cdleme22e  40790  cdleme22eALTN  40791  cdleme42a  40917  cdleme42d  40919  cdlemk20  41320  dih1dimatlem0  41774  lcfrlem2  41989  elrfi  43126  fzsplit1nn0  43186  rabdiophlem2  43230  eldioph4b  43239  diophren  43241  pell1qrgaplem  43301  rngunsnply  43597  oe2  43833  disjinfi  45622  fmuldfeq  46013  limciccioolb  46051  ditgeq3d  46392  stoweidlem44  46472  dirkertrigeq  46529  fourierdlem32  46567  fourierdlem33  46568  fourierdlem42  46577  fourierdlem62  46596  fourierdlem84  46618  fourierdlem85  46619  fourierdlem97  46631  fourierdlem98  46632  fourierdlem102  46636  fourierdlem104  46638  fourierdlem113  46647  fourierdlem114  46648  fourierswlem  46658  fouriersw  46659  sssalgen  46763  meadjun  46890  cos3t  47320  sin5tlem1  47321  fcoreslem2  47512  fnfocofob  47527  deccarry  47759  fsumsplitsndif  47829  gricushgr  48393  ushggricedg  48403  2sphere  49225  iscnrm3rlem1  49415