Theorem eqtr2id 2786

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

Syntax hints:   → wi 4   = wceq 1542

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqtr3di  2788  opeqsng  5504  relop  5851  ordintdif  6415  iotanul  6522  funopg  6583  funcnvres  6627  fpropnf1  7266  csbriota  7381  csbov123  7451  mpocurryd  8254  nneob  8655  sucdom2OLD  9082  pwfilem  9177  sucdom2  9206  unblem2  9296  pwfilemOLD  9346  pr2ne  9999  kmlem2  10146  kmlem11  10155  kmlem12  10156  cflim3  10257  1idsr  11093  recextlem1  11844  quoremz  13820  quoremnn0ALT  13822  intfrac2  13823  hashprg  14355  hashfacen  14413  hashfacenOLD  14414  leiso  14420  ccatrid  14537  repsw2  14901  repsw3  14902  cvgcmpce  15764  explecnv  15811  risefallfac  15968  ramub1lem1  16959  ressress  17193  subsubc  17803  grp1inv  18931  eqg0subg  19073  psgnunilem1  19361  psgn0fv0  19379  psgnsn  19388  efginvrel2  19595  efgredleme  19611  efgcpbllemb  19623  cmnbascntr  19673  frgpnabllem1  19741  gsumzaddlem  19789  gsumzmhm  19805  fsfnn0gsumfsffz  19851  dprd2da  19912  dpjcntz  19922  dpjdisj  19923  dpjlsm  19924  dpjidcl  19928  ablfac1lem  19938  ablfac1eu  19943  ringurd  20008  rnrhmsubrg  20352  lmhmlsp  20660  frlmip  21333  mplmon2mul  21630  1marepvmarrepid  22077  m1detdiag  22099  cramerimplem2  22186  pmatcollpw3lem  22285  chpscmatgsumbin  22346  chpscmatgsummon  22347  cayhamlem2  22386  neitr  22684  fixufil  23426  trust  23734  restmetu  24079  nmfval0  24099  nmval2  24101  rerest  24320  xrrest  24323  xrge0gsumle  24349  rrxip  24907  rrx0  24914  rrxdsfi  24928  voliunlem3  25069  volsup  25073  itg1addlem5  25218  itg2monolem1  25268  itg2cnlem2  25280  itgmpt  25300  iblcnlem1  25305  itgcnlem  25307  itgioo  25333  limcres  25403  mdegfval  25580  dgrlem  25743  coeidlem  25751  mcubic  26352  binom4  26355  dquartlem2  26357  amgm  26495  lgamgulmlem2  26534  eflgam  26549  wilthlem2  26573  rpvmasum2  27015  pntlemo  27110  bday0b  27331  wlkres  28927  3wlkond  29424  3cycld  29431  frgrncvvdeqlem3  29554  vc2OLD  29821  nvge0  29926  nmoo0  30044  bcsiALT  30432  pjchi  30685  shjshseli  30746  spanpr  30833  pjinvari  31444  mdslmd1lem2  31579  iundifdifd  31793  iundifdif  31794  fmptco1f1o  31857  gtiso  31922  gsumhashmul  32208  cycpmco2lem4  32288  cycpmconjslem2  32314  rspsnel  32484  qusima  32519  mxidlirred  32588  zarcls0  32848  esumpr2  33065  omssubaddlem  33298  eulerpartlemt  33370  ofcccat  33554  2cycld  34129  satfv1lem  34353  mpomulcn  35162  topjoin  35250  tailfval  35257  tailf  35260  dvasin  36572  dvacos  36573  opidon2OLD  36722  cdleme4  39109  cdleme22e  39215  cdleme22eALTN  39216  cdleme42a  39342  cdleme42d  39344  cdlemk20  39745  dih1dimatlem0  40199  lcfrlem2  40414  elrfi  41432  fzsplit1nn0  41492  rabdiophlem2  41540  eldioph4b  41549  diophren  41551  pell1qrgaplem  41611  rngunsnply  41915  om2  42155  oe2  42157  disjinfi  43891  fmuldfeq  44299  limciccioolb  44337  ditgeq3d  44680  stoweidlem44  44760  dirkertrigeq  44817  fourierdlem32  44855  fourierdlem33  44856  fourierdlem42  44865  fourierdlem62  44884  fourierdlem84  44906  fourierdlem85  44907  fourierdlem97  44919  fourierdlem98  44920  fourierdlem102  44924  fourierdlem104  44926  fourierdlem113  44935  fourierdlem114  44936  fourierswlem  44946  fouriersw  44947  sssalgen  45051  meadjun  45178  fcoreslem2  45774  fnfocofob  45787  deccarry  46019  fsumsplitsndif  46041  isomushgr  46494  ushrisomgr  46509  funcrngcsetcALT  46897  2sphere  47435  iscnrm3rlem1  47573