Theorem eqtr2id 2809

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

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqtr3di  2811  opeqsng  5469  relop  5818  ordintdif  6391  iotanul  6495  funopg  6549  funcnvres  6593  fpropnf1  7245  csbriota  7362  csbov123  7434  mpocurryd  8242  om2  8548  nneob  8619  sucdom2  9164  unblem2  9230  pwfilem  9255  prfi  9261  pr2ne  9954  kmlem2  10101  kmlem11  10110  kmlem12  10111  cflim3  10212  1idsr  11049  recextlem1  11810  quoremz  13858  quoremnn0ALT  13860  intfrac2  13861  hashprg  14401  hashfacen  14460  leiso  14465  ccatrid  14594  repsw2  14956  repsw3  14957  cvgcmpce  15836  explecnv  15885  risefallfac  16044  ramub1lem1  17052  ressress  17273  subsubc  17876  chnfi  18656  grp1inv  19080  eqg0subg  19227  psgnunilem1  19523  psgn0fv0  19541  psgnsn  19550  efginvrel2  19757  efgredleme  19773  efgcpbllemb  19785  cmnbascntr  19835  frgpnabllem1  19903  gsumzaddlem  19951  gsumzmhm  19967  fsfnn0gsumfsffz  20013  dprd2da  20074  dpjcntz  20084  dpjdisj  20085  dpjlsm  20086  dpjidcl  20090  ablfac1lem  20100  ablfac1eu  20105  ringurd  20221  funcrngcsetcALT  20677  lmhmlsp  21103  elrspsn  21297  frlmip  21817  opsrtoslem2  22096  mplmon2mul  22109  1marepvmarrepid  22622  m1detdiag  22644  cramerimplem2  22731  pmatcollpw3lem  22830  chpscmatgsumbin  22891  chpscmatgsummon  22892  cayhamlem2  22931  neitr  23227  fixufil  23969  trust  24276  restmetu  24617  nmfval0  24637  nmval2  24639  rerest  24851  xrrest  24855  xrge0gsumle  24881  mpomulcn  24916  rrxip  25439  rrx0  25446  rrxdsfi  25460  voliunlem3  25601  volsup  25605  itg1addlem5  25749  itg2monolem1  25799  itg2cnlem2  25811  itgmpt  25832  iblcnlem1  25837  itgcnlem  25839  itgioo  25865  limcres  25935  mdegfval  26109  dgrlem  26276  coeidlem  26284  mcubic  26899  binom4  26902  dquartlem2  26904  amgm  27042  lgamgulmlem2  27081  eflgam  27096  wilthlem2  27120  rpvmasum2  27563  pntlemo  27658  bday0b  27893  pw2cut2  28542  zz12s  28555  wlkres  29825  3wlkond  30329  3cycld  30336  frgrncvvdeqlem3  30459  vc2OLD  30727  nvge0  30832  nmoo0  30950  bcsiALT  31338  pjchi  31591  shjshseli  31652  spanpr  31739  pjinvari  32350  mdslmd1lem2  32485  iundifdifd  32720  iundifdif  32721  fresunsn  32787  fmptco1f1o  32795  gtiso  32863  gsumhashmul  33207  cycpmco2lem4  33269  cycpmconjslem2  33295  qusima  33554  mxidlirred  33620  selvascl  33774  esplyind  33832  vietalem  33836  extdgfialglem1  33949  2sqr3minply  34037  zarcls0  34125  esumpr2  34324  omssubaddlem  34556  eulerpartlemt  34628  ofcccat  34800  2cycld  35448  satfv1lem  35672  topjoin  36685  tailfval  36692  tailf  36695  dvasin  38163  dvacos  38164  opidon2OLD  38313  cdleme4  40822  cdleme22e  40928  cdleme22eALTN  40929  cdleme42a  41055  cdleme42d  41057  cdlemk20  41458  dih1dimatlem0  41912  lcfrlem2  42127  elrfi  43235  fzsplit1nn0  43295  rabdiophlem2  43339  eldioph4b  43348  diophren  43350  pell1qrgaplem  43410  rngunsnply  43706  oe2  43942  disjinfi  45730  fmuldfeq  46119  limciccioolb  46157  ditgeq3d  46498  stoweidlem44  46578  dirkertrigeq  46635  fourierdlem32  46673  fourierdlem33  46674  fourierdlem42  46683  fourierdlem62  46702  fourierdlem84  46724  fourierdlem85  46725  fourierdlem97  46737  fourierdlem98  46738  fourierdlem102  46742  fourierdlem104  46744  fourierdlem113  46753  fourierdlem114  46754  fourierswlem  46764  fouriersw  46765  sssalgen  46869  meadjun  46996  cos3t  47426  sin5tlem1  47427  fcoreslem2  47618  fnfocofob  47633  deccarry  47865  fsumsplitsndif  47935  gricushgr  48499  ushggricedg  48509  2sphere  49331  iscnrm3rlem1  49521