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 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqtr3di  2813  opeqsng  5488  relop  5838  ordintdif  6414  iotanul  6518  funopg  6572  funcnvres  6616  fpropnf1  7267  csbriota  7384  csbov123  7456  mpocurryd  8266  om2  8572  nneob  8643  sucdom2  9188  unblem2  9254  pwfilem  9278  prfi  9284  pr2ne  9990  kmlem2  10136  kmlem11  10145  kmlem12  10146  cflim3  10247  1idsr  11084  recextlem1  11845  quoremz  13890  quoremnn0ALT  13892  intfrac2  13893  hashprg  14433  hashfacen  14493  leiso  14498  ccatrid  14627  repsw2  14989  repsw3  14990  cvgcmpce  15872  explecnv  15921  risefallfac  16080  ramub1lem1  17087  ressress  17308  subsubc  17911  chnfi  18691  grp1inv  19115  eqg0subg  19268  psgnunilem1  19564  psgn0fv0  19582  psgnsn  19591  efginvrel2  19798  efgredleme  19814  efgcpbllemb  19826  cmnbascntr  19876  frgpnabllem1  19944  gsumzaddlem  19992  gsumzmhm  20008  fsfnn0gsumfsffz  20054  dprd2da  20115  dpjcntz  20125  dpjdisj  20126  dpjlsm  20127  dpjidcl  20131  ablfac1lem  20141  ablfac1eu  20146  ringurd  20268  funcrngcsetcALT  20727  lmhmlsp  21151  elrspsn  21352  frlmip  21909  opsrtoslem2  22188  mplmon2mul  22201  1marepvmarrepid  22713  m1detdiag  22735  cramerimplem2  22822  pmatcollpw3lem  22921  chpscmatgsumbin  22982  chpscmatgsummon  22983  cayhamlem2  23022  neitr  23318  fixufil  24060  trust  24367  restmetu  24708  nmfval0  24728  nmval2  24730  rerest  24942  xrrest  24946  xrge0gsumle  24972  mpomulcn  25007  rrxip  25530  rrx0  25537  rrxdsfi  25551  voliunlem3  25692  volsup  25696  itg1addlem5  25840  itg2monolem1  25890  itg2cnlem2  25902  itgmpt  25923  iblcnlem1  25928  itgcnlem  25930  itgioo  25956  limcres  26026  mdegfval  26200  dgrlem  26367  coeidlem  26375  mcubic  26993  binom4  26996  dquartlem2  26998  amgm  27136  lgamgulmlem2  27175  eflgam  27190  wilthlem2  27214  rpvmasum2  27657  pntlemo  27752  bday0b  27987  pw2cut2  28636  zz12s  28649  wlkres  29999  3wlkond  30503  3cycld  30510  frgrncvvdeqlem3  30633  vc2OLD  30901  nvge0  31006  nmoo0  31124  bcsiALT  31512  pjchi  31765  shjshseli  31826  spanpr  31913  pjinvari  32524  mdslmd1lem2  32659  iundifdifd  32887  iundifdif  32888  fresunsn  32951  fmptco1f1o  32959  gtiso  33027  gsumhashmul  33368  cycpmco2lem4  33430  cycpmconjslem2  33456  qusima  33698  mxidlirred  33736  selvascl  33888  esplyind  33946  vietalem  33950  extdgfialglem1  34063  2sqr3minply  34151  zarcls0  34239  esumpr2  34438  omssubaddlem  34670  eulerpartlemt  34742  ofcccat  34914  2cycld  35611  satfv1lem  35835  topjoin  36857  tailfval  36864  tailf  36867  dvasin  38336  dvacos  38337  opidon2OLD  38486  cdleme4  40993  cdleme22e  41099  cdleme22eALTN  41100  cdleme42a  41226  cdleme42d  41228  cdlemk20  41629  dih1dimatlem0  42083  lcfrlem2  42298  elrfi  43408  fzsplit1nn0  43468  rabdiophlem2  43512  eldioph4b  43521  diophren  43523  pell1qrgaplem  43583  rngunsnply  43879  oe2  44115  disjinfi  45893  fmuldfeq  46282  limciccioolb  46320  ditgeq3d  46661  stoweidlem44  46741  dirkertrigeq  46798  fourierdlem32  46836  fourierdlem33  46837  fourierdlem42  46846  fourierdlem62  46865  fourierdlem84  46887  fourierdlem85  46888  fourierdlem97  46900  fourierdlem98  46901  fourierdlem102  46905  fourierdlem104  46907  fourierdlem113  46916  fourierdlem114  46917  fourierswlem  46927  fouriersw  46928  sssalgen  47032  meadjun  47159  cos3t  47592  sin5tlem1  47593  fcoreslem2  47784  fnfocofob  47799  deccarry  48031  fsumsplitsndif  48101  gricushgr  48665  ushggricedg  48675  2sphere  49512  iscnrm3rlem1  49701