Theorem eqtr2id 2777

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

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716

This theorem is referenced by:  eqtr3di  2779  opeqsng  5494  relop  5841  ordintdif  6405  iotanul  6512  funopg  6573  funcnvres  6617  fpropnf1  7259  csbriota  7374  csbov123  7444  mpocurryd  8250  nneob  8652  sucdom2OLD  9079  pwfilem  9174  sucdom2  9203  unblem2  9293  pwfilemOLD  9343  pr2ne  9996  kmlem2  10143  kmlem11  10152  kmlem12  10153  cflim3  10254  1idsr  11090  recextlem1  11842  quoremz  13818  quoremnn0ALT  13820  intfrac2  13821  hashprg  14353  hashfacen  14411  hashfacenOLD  14412  leiso  14418  ccatrid  14535  repsw2  14899  repsw3  14900  cvgcmpce  15762  explecnv  15809  risefallfac  15966  ramub1lem1  16960  ressress  17194  subsubc  17804  grp1inv  18968  eqg0subg  19114  psgnunilem1  19405  psgn0fv0  19423  psgnsn  19432  efginvrel2  19639  efgredleme  19655  efgcpbllemb  19667  cmnbascntr  19717  frgpnabllem1  19785  gsumzaddlem  19833  gsumzmhm  19849  fsfnn0gsumfsffz  19895  dprd2da  19956  dpjcntz  19966  dpjdisj  19967  dpjlsm  19968  dpjidcl  19972  ablfac1lem  19982  ablfac1eu  19987  ringurd  20082  rnrhmsubrg  20499  funcrngcsetcALT  20529  lmhmlsp  20889  frlmip  21643  mplmon2mul  21942  1marepvmarrepid  22401  m1detdiag  22423  cramerimplem2  22510  pmatcollpw3lem  22609  chpscmatgsumbin  22670  chpscmatgsummon  22671  cayhamlem2  22710  neitr  23008  fixufil  23750  trust  24058  restmetu  24403  nmfval0  24423  nmval2  24425  rerest  24644  xrrest  24647  xrge0gsumle  24673  mpomulcn  24709  rrxip  25242  rrx0  25249  rrxdsfi  25263  voliunlem3  25405  volsup  25409  itg1addlem5  25554  itg2monolem1  25604  itg2cnlem2  25616  itgmpt  25636  iblcnlem1  25641  itgcnlem  25643  itgioo  25669  limcres  25739  mdegfval  25922  dgrlem  26085  coeidlem  26093  mcubic  26698  binom4  26701  dquartlem2  26703  amgm  26842  lgamgulmlem2  26881  eflgam  26896  wilthlem2  26920  rpvmasum2  27364  pntlemo  27459  bday0b  27682  wlkres  29399  3wlkond  29896  3cycld  29903  frgrncvvdeqlem3  30026  vc2OLD  30293  nvge0  30398  nmoo0  30516  bcsiALT  30904  pjchi  31157  shjshseli  31218  spanpr  31305  pjinvari  31916  mdslmd1lem2  32051  iundifdifd  32265  iundifdif  32266  fmptco1f1o  32329  gtiso  32394  gsumhashmul  32679  cycpmco2lem4  32759  cycpmconjslem2  32785  rspsnel  32956  qusima  32991  mxidlirred  33060  zarcls0  33340  esumpr2  33557  omssubaddlem  33790  eulerpartlemt  33862  ofcccat  34046  2cycld  34620  satfv1lem  34844  topjoin  35741  tailfval  35748  tailf  35751  dvasin  37066  dvacos  37067  opidon2OLD  37216  cdleme4  39603  cdleme22e  39709  cdleme22eALTN  39710  cdleme42a  39836  cdleme42d  39838  cdlemk20  40239  dih1dimatlem0  40693  lcfrlem2  40908  elrfi  41946  fzsplit1nn0  42006  rabdiophlem2  42054  eldioph4b  42063  diophren  42065  pell1qrgaplem  42125  rngunsnply  42429  om2  42669  oe2  42671  disjinfi  44401  fmuldfeq  44809  limciccioolb  44847  ditgeq3d  45190  stoweidlem44  45270  dirkertrigeq  45327  fourierdlem32  45365  fourierdlem33  45366  fourierdlem42  45375  fourierdlem62  45394  fourierdlem84  45416  fourierdlem85  45417  fourierdlem97  45429  fourierdlem98  45430  fourierdlem102  45434  fourierdlem104  45436  fourierdlem113  45445  fourierdlem114  45446  fourierswlem  45456  fouriersw  45457  sssalgen  45561  meadjun  45688  fcoreslem2  46284  fnfocofob  46297  deccarry  46529  fsumsplitsndif  46551  isomushgr  47004  ushrisomgr  47019  2sphere  47648  iscnrm3rlem1  47785