Theorem eqtr2id 2792

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  eqtr3di  2794  opeqsng  5418  relop  5762  ordintdif  6319  iotanul  6415  funopg  6475  funcnvres  6519  fpropnf1  7149  csbriota  7257  csbov123  7326  mpocurryd  8094  nneob  8495  sucdom2OLD  8878  pwfilem  8969  sucdom2  8998  unblem2  9076  pwfilemOLD  9122  kmlem2  9916  kmlem11  9925  kmlem12  9926  cflim3  10027  1idsr  10863  recextlem1  11614  quoremz  13584  quoremnn0ALT  13586  intfrac2  13587  hashprg  14119  hashfacen  14175  hashfacenOLD  14176  leiso  14182  ccatrid  14301  repsw2  14672  repsw3  14673  cvgcmpce  15539  explecnv  15586  risefallfac  15743  ramub1lem1  16736  ressress  16967  subsubc  17577  grp1inv  18692  psgnunilem1  19110  psgn0fv0  19128  psgnsn  19137  efginvrel2  19342  efgredleme  19358  efgcpbllemb  19370  frgpnabllem1  19483  gsumzaddlem  19531  gsumzmhm  19547  fsfnn0gsumfsffz  19593  dprd2da  19654  dpjcntz  19664  dpjdisj  19665  dpjlsm  19666  dpjidcl  19670  ablfac1lem  19680  ablfac1eu  19685  rnrhmsubrg  20065  lmhmlsp  20320  frlmip  20994  mplmon2mul  21286  1marepvmarrepid  21733  m1detdiag  21755  cramerimplem2  21842  pmatcollpw3lem  21941  chpscmatgsumbin  22002  chpscmatgsummon  22003  cayhamlem2  22042  neitr  22340  fixufil  23082  trust  23390  restmetu  23735  nmfval0  23755  nmval2  23757  rerest  23976  xrrest  23979  xrge0gsumle  24005  rrxip  24563  rrx0  24570  rrxdsfi  24584  voliunlem3  24725  volsup  24729  itg1addlem5  24874  itg2monolem1  24924  itg2cnlem2  24936  itgmpt  24956  iblcnlem1  24961  itgcnlem  24963  itgioo  24989  limcres  25059  mdegfval  25236  dgrlem  25399  coeidlem  25407  mcubic  26006  binom4  26009  dquartlem2  26011  amgm  26149  lgamgulmlem2  26188  eflgam  26203  wilthlem2  26227  rpvmasum2  26669  pntlemo  26764  wlkres  28047  3wlkond  28544  3cycld  28551  frgrncvvdeqlem3  28674  vc2OLD  28939  nvge0  29044  nmoo0  29162  bcsiALT  29550  pjchi  29803  shjshseli  29864  spanpr  29951  pjinvari  30562  mdslmd1lem2  30697  iundifdifd  30910  iundifdif  30911  fmptco1f1o  30977  gtiso  31042  gsumhashmul  31325  cycpmco2lem4  31405  cycpmconjslem2  31431  rngurd  31491  rspsnel  31576  qusima  31603  zarcls0  31827  esumpr2  32044  omssubaddlem  32275  eulerpartlemt  32347  ofcccat  32531  2cycld  33109  satfv1lem  33333  bday0b  34033  topjoin  34563  tailfval  34570  tailf  34573  dvasin  35870  dvacos  35871  opidon2OLD  36021  cdleme4  38259  cdleme22e  38365  cdleme22eALTN  38366  cdleme42a  38492  cdleme42d  38494  cdlemk20  38895  dih1dimatlem0  39349  lcfrlem2  39564  elrfi  40523  fzsplit1nn0  40583  rabdiophlem2  40631  eldioph4b  40640  diophren  40642  pell1qrgaplem  40702  rngunsnply  41005  disjinfi  42738  fmuldfeq  43131  limciccioolb  43169  ditgeq3d  43512  stoweidlem44  43592  dirkertrigeq  43649  fourierdlem32  43687  fourierdlem33  43688  fourierdlem42  43697  fourierdlem62  43716  fourierdlem84  43738  fourierdlem85  43739  fourierdlem97  43751  fourierdlem98  43752  fourierdlem102  43756  fourierdlem104  43758  fourierdlem113  43767  fourierdlem114  43768  fourierswlem  43778  fouriersw  43779  sssalgen  43881  meadjun  44007  fcoreslem2  44569  fnfocofob  44582  deccarry  44814  fsumsplitsndif  44836  isomushgr  45289  ushrisomgr  45304  funcrngcsetcALT  45568  2sphere  46106  iscnrm3rlem1  46245