Theorem eqtr2id 2790

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  eqtr3di  2792  opeqsng  5508  relop  5861  ordintdif  6434  iotanul  6539  funopg  6600  funcnvres  6644  fpropnf1  7287  csbriota  7403  csbov123  7475  mpocurryd  8294  nneob  8694  sucdom2OLD  9122  sucdom2  9243  unblem2  9329  pwfilem  9356  prfi  9363  pr2ne  10044  kmlem2  10192  kmlem11  10201  kmlem12  10202  cflim3  10302  1idsr  11138  recextlem1  11893  quoremz  13895  quoremnn0ALT  13897  intfrac2  13898  hashprg  14434  hashfacen  14493  leiso  14498  ccatrid  14625  repsw2  14989  repsw3  14990  cvgcmpce  15854  explecnv  15901  risefallfac  16060  ramub1lem1  17064  ressress  17293  subsubc  17898  grp1inv  19066  eqg0subg  19214  psgnunilem1  19511  psgn0fv0  19529  psgnsn  19538  efginvrel2  19745  efgredleme  19761  efgcpbllemb  19773  cmnbascntr  19823  frgpnabllem1  19891  gsumzaddlem  19939  gsumzmhm  19955  fsfnn0gsumfsffz  20001  dprd2da  20062  dpjcntz  20072  dpjdisj  20073  dpjlsm  20074  dpjidcl  20078  ablfac1lem  20088  ablfac1eu  20093  ringurd  20182  funcrngcsetcALT  20641  lmhmlsp  21048  elrspsn  21250  frlmip  21798  opsrtoslem2  22080  mplmon2mul  22093  1marepvmarrepid  22581  m1detdiag  22603  cramerimplem2  22690  pmatcollpw3lem  22789  chpscmatgsumbin  22850  chpscmatgsummon  22851  cayhamlem2  22890  neitr  23188  fixufil  23930  trust  24238  restmetu  24583  nmfval0  24603  nmval2  24605  rerest  24825  xrrest  24829  xrge0gsumle  24855  mpomulcn  24891  rrxip  25424  rrx0  25431  rrxdsfi  25445  voliunlem3  25587  volsup  25591  itg1addlem5  25735  itg2monolem1  25785  itg2cnlem2  25797  itgmpt  25818  iblcnlem1  25823  itgcnlem  25825  itgioo  25851  limcres  25921  mdegfval  26101  dgrlem  26268  coeidlem  26276  mcubic  26890  binom4  26893  dquartlem2  26895  amgm  27034  lgamgulmlem2  27073  eflgam  27088  wilthlem2  27112  rpvmasum2  27556  pntlemo  27651  bday0b  27875  zzs12  28423  wlkres  29688  3wlkond  30190  3cycld  30197  frgrncvvdeqlem3  30320  vc2OLD  30587  nvge0  30692  nmoo0  30810  bcsiALT  31198  pjchi  31451  shjshseli  31512  spanpr  31599  pjinvari  32210  mdslmd1lem2  32345  iundifdifd  32574  iundifdif  32575  fmptco1f1o  32643  gtiso  32710  gsumhashmul  33064  cycpmco2lem4  33149  cycpmconjslem2  33175  qusima  33436  mxidlirred  33500  2sqr3minply  33791  zarcls0  33867  esumpr2  34068  omssubaddlem  34301  eulerpartlemt  34373  ofcccat  34558  2cycld  35143  satfv1lem  35367  topjoin  36366  tailfval  36373  tailf  36376  dvasin  37711  dvacos  37712  opidon2OLD  37861  cdleme4  40240  cdleme22e  40346  cdleme22eALTN  40347  cdleme42a  40473  cdleme42d  40475  cdlemk20  40876  dih1dimatlem0  41330  lcfrlem2  41545  elrfi  42705  fzsplit1nn0  42765  rabdiophlem2  42813  eldioph4b  42822  diophren  42824  pell1qrgaplem  42884  rngunsnply  43181  om2  43417  oe2  43419  disjinfi  45197  fmuldfeq  45598  limciccioolb  45636  ditgeq3d  45979  stoweidlem44  46059  dirkertrigeq  46116  fourierdlem32  46154  fourierdlem33  46155  fourierdlem42  46164  fourierdlem62  46183  fourierdlem84  46205  fourierdlem85  46206  fourierdlem97  46218  fourierdlem98  46219  fourierdlem102  46223  fourierdlem104  46225  fourierdlem113  46234  fourierdlem114  46235  fourierswlem  46245  fouriersw  46246  sssalgen  46350  meadjun  46477  fcoreslem2  47076  fnfocofob  47091  deccarry  47323  fsumsplitsndif  47360  gricushgr  47886  ushggricedg  47896  2sphere  48670  iscnrm3rlem1  48837