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 ⊢ (𝜑 → 𝐶 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqtr3di  2811  opeqsng  5475  relop  5828  ordintdif  6407  iotanul  6511  funopg  6566  funcnvres  6610  fpropnf1  7263  csbriota  7384  csbov123  7456  mpocurryd  8270  om2  8578  nneob  8649  sucdom2  9202  unblem2  9269  pwfilem  9293  prfi  9299  pr2ne  10065  kmlem2  10211  kmlem11  10220  kmlem12  10221  cflim3  10321  1idsr  11164  recextlem1  11927  quoremz  13975  quoremnn0ALT  13977  intfrac2  13978  hashprg  14519  hashfacen  14579  leiso  14584  ccatrid  14713  repsw2  15083  repsw3  15084  cvgcmpce  15965  explecnv  16014  risefallfac  16171  ramub1lem1  17184  ressress  17405  subsubc  18008  chnfi  18788  grp1inv  19238  eqg0subg  19391  psgnunilem1  19687  psgn0fv0  19705  psgnsn  19714  efginvrel2  19921  efgredleme  19937  efgcpbllemb  19949  cmnbascntr  19999  frgpnabllem1  20067  gsumzaddlem  20115  gsumzmhm  20131  fsfnn0gsumfsffz  20177  dprd2da  20238  dpjcntz  20248  dpjdisj  20249  dpjlsm  20250  dpjidcl  20254  ablfac1lem  20264  ablfac1eu  20269  ringurd  20391  funcrngcsetcALT  20873  lmhmlsp  21304  elrspsn  21505  frlmip  22064  opsrtoslem2  22345  mplmon2mul  22358  1marepvmarrepid  22870  m1detdiag  22892  cramerimplem2  22982  pmatcollpw3lem  23081  chpscmatgsumbin  23142  chpscmatgsummon  23143  cayhamlem2  23182  neitr  23478  fixufil  24221  trust  24528  restmetu  24869  nmfval0  24889  nmval2  24891  rerest  25103  xrrest  25107  xrge0gsumle  25133  mpomulcn  25168  rrxip  25691  rrx0  25698  rrxdsfi  25712  voliunlem3  25853  volsup  25857  itg1addlem5  26001  itg2monolem1  26051  itg2cnlem2  26063  itgmpt  26083  iblcnlem1  26088  itgcnlem  26090  itgioo  26116  limcres  26186  mdegfval  26360  dgrlem  26528  coeidlem  26536  mcubic  27157  binom4  27160  dquartlem2  27162  amgm  27300  lgamgulmlem2  27339  eflgam  27354  wilthlem2  27378  rpvmasum2  27821  pntlemo  27916  bday0b  28181  pw2cut2  28830  zz12s  28843  wlkres  30231  2cycld  30727  3wlkond  30754  3cycld  30761  frgrncvvdeqlem3  30884  vc2OLD  31152  nvge0  31257  nmoo0  31375  bcsiALT  31763  pjchi  32016  shjshseli  32077  spanpr  32164  pjinvari  32775  mdslmd1lem2  32910  iundifdifd  33138  iundifdif  33139  fresunsn  33201  fmptco1f1o  33209  gtiso  33276  gsumhashmul  33610  cycpmco2lem4  33672  cycpmconjslem2  33698  qusima  33941  mxidlirred  33979  selvascl  34131  esplyind  34189  vietalem  34193  extdgfialglem1  34306  2sqr3minply  34394  zarcls0  34482  esumpr2  34681  omssubaddlem  34914  eulerpartlemt  34986  ofcccat  35158  satfv1lem  36096  topjoin  37123  tailfval  37130  tailf  37133  dvasin  38590  dvacos  38591  opidon2OLD  38756  cdleme4  41263  cdleme22e  41369  cdleme22eALTN  41370  cdleme42a  41496  cdleme42d  41498  cdlemk20  41899  dih1dimatlem0  42353  lcfrlem2  42568  elrfi  43658  fzsplit1nn0  43718  rabdiophlem2  43762  eldioph4b  43771  diophren  43773  pell1qrgaplem  43833  rngunsnply  44129  oe2  44365  disjinfi  46150  fmuldfeq  46539  limciccioolb  46577  ditgeq3d  46918  stoweidlem44  46998  dirkertrigeq  47055  fourierdlem32  47093  fourierdlem33  47094  fourierdlem42  47103  fourierdlem62  47122  fourierdlem84  47144  fourierdlem85  47145  fourierdlem97  47157  fourierdlem98  47158  fourierdlem102  47162  fourierdlem104  47164  fourierdlem113  47173  fourierdlem114  47174  fourierswlem  47184  fouriersw  47185  sssalgen  47289  meadjun  47416  cos3t  47862  sin5tlem1  47863  fcoreslem2  48078  fnfocofob  48093  deccarry  48325  fsumsplitsndif  48395  gricushgr  48959  ushggricedg  48969  2sphere  49805  iscnrm3rlem1  49992