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 2790	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2744	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqtr3di  2794  opeqsng  5411  relop  5748  ordintdif  6300  iotanul  6396  funopg  6452  funcnvres  6496  fpropnf1  7121  csbriota  7228  csbov123  7297  mpocurryd  8056  nneob  8446  sucdom2  8822  pwfilem  8922  unblem2  8997  pwfilemOLD  9043  kmlem2  9838  kmlem11  9847  kmlem12  9848  cflim3  9949  1idsr  10785  recextlem1  11535  quoremz  13503  quoremnn0ALT  13505  intfrac2  13506  hashprg  14038  hashfacen  14094  hashfacenOLD  14095  leiso  14101  ccatrid  14220  repsw2  14591  repsw3  14592  cvgcmpce  15458  explecnv  15505  risefallfac  15662  ramub1lem1  16655  ressress  16884  subsubc  17484  grp1inv  18598  psgnunilem1  19016  psgn0fv0  19034  psgnsn  19043  efginvrel2  19248  efgredleme  19264  efgcpbllemb  19276  frgpnabllem1  19389  gsumzaddlem  19437  gsumzmhm  19453  fsfnn0gsumfsffz  19499  dprd2da  19560  dpjcntz  19570  dpjdisj  19571  dpjlsm  19572  dpjidcl  19576  ablfac1lem  19586  ablfac1eu  19591  rnrhmsubrg  19971  lmhmlsp  20226  frlmip  20895  mplmon2mul  21187  1marepvmarrepid  21632  m1detdiag  21654  cramerimplem2  21741  pmatcollpw3lem  21840  chpscmatgsumbin  21901  chpscmatgsummon  21902  cayhamlem2  21941  neitr  22239  fixufil  22981  trust  23289  restmetu  23632  nmfval0  23652  nmval2  23654  rerest  23873  xrrest  23876  xrge0gsumle  23902  rrxip  24459  rrx0  24466  rrxdsfi  24480  voliunlem3  24621  volsup  24625  itg1addlem5  24770  itg2monolem1  24820  itg2cnlem2  24832  itgmpt  24852  iblcnlem1  24857  itgcnlem  24859  itgioo  24885  limcres  24955  mdegfval  25132  dgrlem  25295  coeidlem  25303  mcubic  25902  binom4  25905  dquartlem2  25907  amgm  26045  lgamgulmlem2  26084  eflgam  26099  wilthlem2  26123  rpvmasum2  26565  pntlemo  26660  wlkres  27940  3wlkond  28436  3cycld  28443  frgrncvvdeqlem3  28566  vc2OLD  28831  nvge0  28936  nmoo0  29054  bcsiALT  29442  pjchi  29695  shjshseli  29756  spanpr  29843  pjinvari  30454  mdslmd1lem2  30589  iundifdifd  30802  iundifdif  30803  fmptco1f1o  30869  gtiso  30935  gsumhashmul  31218  cycpmco2lem4  31298  cycpmconjslem2  31324  rngurd  31384  rspsnel  31469  qusima  31496  zarcls0  31720  esumpr2  31935  omssubaddlem  32166  eulerpartlemt  32238  ofcccat  32422  2cycld  33000  satfv1lem  33224  bday0b  33951  topjoin  34481  tailfval  34488  tailf  34491  dvasin  35788  dvacos  35789  opidon2OLD  35939  cdleme4  38179  cdleme22e  38285  cdleme22eALTN  38286  cdleme42a  38412  cdleme42d  38414  cdlemk20  38815  dih1dimatlem0  39269  lcfrlem2  39484  elrfi  40432  fzsplit1nn0  40492  rabdiophlem2  40540  eldioph4b  40549  diophren  40551  pell1qrgaplem  40611  rngunsnply  40914  disjinfi  42620  fmuldfeq  43014  limciccioolb  43052  ditgeq3d  43395  stoweidlem44  43475  dirkertrigeq  43532  fourierdlem32  43570  fourierdlem33  43571  fourierdlem42  43580  fourierdlem62  43599  fourierdlem84  43621  fourierdlem85  43622  fourierdlem97  43634  fourierdlem98  43635  fourierdlem102  43639  fourierdlem104  43641  fourierdlem113  43650  fourierdlem114  43651  fourierswlem  43661  fouriersw  43662  sssalgen  43764  meadjun  43890  fcoreslem2  44445  fnfocofob  44458  deccarry  44691  fsumsplitsndif  44713  isomushgr  45166  ushrisomgr  45181  funcrngcsetcALT  45445  2sphere  45983  iscnrm3rlem1  46122