Theorem eqtr2id 2811

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 2810	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2769	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqtr3di  2813  opeqsng  5480  relop  5835  cnvimassrndm  6092  ordintdif  6435  iotanul  6540  funopg  6597  funcnvres  6643  fpropnf1  7297  csbriota  7418  csbov123  7490  mpocurryd  8317  om2  8625  nneob  8696  sucdom2  9249  unblem2  9316  pwfilem  9340  prfi  9346  pr2ne  10114  kmlem2  10260  kmlem11  10269  kmlem12  10270  cflim3  10370  1idsr  11213  recextlem1  11976  quoremz  14025  quoremnn0ALT  14027  intfrac2  14028  hashprg  14569  hashfacen  14629  leiso  14634  ccatrid  14763  repsw2  15135  repsw3  15136  cvgcmpce  16017  explecnv  16066  risefallfac  16223  ramub1lem1  17236  ressress  17457  subsubc  18060  chnfi  18840  grp1inv  19290  eqg0subg  19443  psgnunilem1  19740  psgn0fv0  19758  psgnsn  19767  efginvrel2  19974  efgredleme  19990  efgcpbllemb  20002  cmnbascntr  20052  frgpnabllem1  20120  gsumzaddlem  20168  gsumzmhm  20184  fsfnn0gsumfsffz  20230  dprd2da  20291  dpjcntz  20301  dpjdisj  20302  dpjlsm  20303  dpjidcl  20307  ablfac1lem  20317  ablfac1eu  20322  ringurd  20444  funcrngcsetcALT  20926  lmhmlsp  21357  elrspsn  21558  frlmip  22117  opsrtoslem2  22398  mplmon2mul  22411  1marepvmarrepid  22923  m1detdiag  22945  cramerimplem2  23035  pmatcollpw3lem  23134  chpscmatgsumbin  23195  chpscmatgsummon  23196  cayhamlem2  23235  neitr  23531  fixufil  24274  trust  24581  restmetu  24922  nmfval0  24942  nmval2  24944  rerest  25156  xrrest  25160  xrge0gsumle  25186  mpomulcn  25221  rrxip  25744  rrx0  25751  rrxdsfi  25765  voliunlem3  25906  volsup  25910  itg1addlem5  26054  itg2monolem1  26104  itg2cnlem2  26116  itgmpt  26136  iblcnlem1  26141  itgcnlem  26143  itgioo  26169  limcres  26239  mdegfval  26413  dgrlem  26581  coeidlem  26589  mcubic  27208  binom4  27211  dquartlem2  27213  amgm  27351  lgamgulmlem2  27390  eflgam  27405  wilthlem2  27429  rpvmasum2  27872  pntlemo  27967  bday0b  28232  pw2cut2  28881  zz12s  28894  wlkres  30282  2cycld  30778  3wlkond  30805  3cycld  30812  frgrncvvdeqlem3  30935  vc2OLD  31203  nvge0  31308  nmoo0  31426  bcsiALT  31814  pjchi  32067  shjshseli  32128  spanpr  32215  pjinvari  32826  mdslmd1lem2  32961  iundifdifd  33231  iundifdif  33232  fresunsn  33294  fmptco1f1o  33302  gtiso  33368  gsumhashmul  33704  cycpmco2lem4  33766  cycpmconjslem2  33792  isedom  33934  qusima  34043  mxidlirred  34081  selvascl  34232  esplyind  34290  vietalem  34294  extdgfialglem1  34407  2sqr3minply  34495  zarcls0  34583  esumpr2  34782  omssubaddlem  35014  eulerpartlemt  35086  ofcccat  35258  satfv1lem  36307  topjoin  37344  tailfval  37351  tailf  37354  dvasin  38827  dvacos  38828  opidon2OLD  38991  cdleme4  41498  cdleme22e  41604  cdleme22eALTN  41605  cdleme42a  41731  cdleme42d  41733  cdlemk20  42134  dih1dimatlem0  42588  lcfrlem2  42803  elrfi  43909  fzsplit1nn0  43969  rabdiophlem2  44013  eldioph4b  44022  diophren  44024  pell1qrgaplem  44084  rngunsnply  44374  oe2  44610  disjinfi  46422  fmuldfeq  46810  limciccioolb  46848  ditgeq3d  47189  stoweidlem44  47269  dirkertrigeq  47326  fourierdlem32  47364  fourierdlem33  47365  fourierdlem42  47374  fourierdlem62  47393  fourierdlem84  47415  fourierdlem85  47416  fourierdlem97  47428  fourierdlem98  47429  fourierdlem102  47433  fourierdlem104  47435  fourierdlem113  47444  fourierdlem114  47445  fourierswlem  47455  fouriersw  47456  sssalgen  47560  meadjun  47687  cos3t  48133  sin5tlem1  48134  fcoreslem2  48349  fnfocofob  48364  deccarry  48596  fsumsplitsndif  48666  gricushgr  49230  ushggricedg  49240  2sphere  50076  iscnrm3rlem1  50269