Theorem eqtr2id 2793

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqtr3di  2795  opeqsng  5522  relop  5875  ordintdif  6445  iotanul  6551  funopg  6612  funcnvres  6656  fpropnf1  7304  csbriota  7420  csbov123  7492  mpocurryd  8310  nneob  8712  sucdom2OLD  9148  sucdom2  9269  unblem2  9357  pwfilem  9384  prfi  9391  pwfilemOLD  9416  pr2ne  10073  kmlem2  10221  kmlem11  10230  kmlem12  10231  cflim3  10331  1idsr  11167  recextlem1  11920  quoremz  13906  quoremnn0ALT  13908  intfrac2  13909  hashprg  14444  hashfacen  14503  leiso  14508  ccatrid  14635  repsw2  14999  repsw3  15000  cvgcmpce  15866  explecnv  15913  risefallfac  16072  ramub1lem1  17073  ressress  17307  subsubc  17917  grp1inv  19088  eqg0subg  19236  psgnunilem1  19535  psgn0fv0  19553  psgnsn  19562  efginvrel2  19769  efgredleme  19785  efgcpbllemb  19797  cmnbascntr  19847  frgpnabllem1  19915  gsumzaddlem  19963  gsumzmhm  19979  fsfnn0gsumfsffz  20025  dprd2da  20086  dpjcntz  20096  dpjdisj  20097  dpjlsm  20098  dpjidcl  20102  ablfac1lem  20112  ablfac1eu  20117  ringurd  20212  funcrngcsetcALT  20663  lmhmlsp  21071  elrspsn  21273  frlmip  21821  opsrtoslem2  22103  mplmon2mul  22116  1marepvmarrepid  22602  m1detdiag  22624  cramerimplem2  22711  pmatcollpw3lem  22810  chpscmatgsumbin  22871  chpscmatgsummon  22872  cayhamlem2  22911  neitr  23209  fixufil  23951  trust  24259  restmetu  24604  nmfval0  24624  nmval2  24626  rerest  24845  xrrest  24848  xrge0gsumle  24874  mpomulcn  24910  rrxip  25443  rrx0  25450  rrxdsfi  25464  voliunlem3  25606  volsup  25610  itg1addlem5  25755  itg2monolem1  25805  itg2cnlem2  25817  itgmpt  25838  iblcnlem1  25843  itgcnlem  25845  itgioo  25871  limcres  25941  mdegfval  26121  dgrlem  26288  coeidlem  26296  mcubic  26908  binom4  26911  dquartlem2  26913  amgm  27052  lgamgulmlem2  27091  eflgam  27106  wilthlem2  27130  rpvmasum2  27574  pntlemo  27669  bday0b  27893  zzs12  28441  wlkres  29706  3wlkond  30203  3cycld  30210  frgrncvvdeqlem3  30333  vc2OLD  30600  nvge0  30705  nmoo0  30823  bcsiALT  31211  pjchi  31464  shjshseli  31525  spanpr  31612  pjinvari  32223  mdslmd1lem2  32358  iundifdifd  32584  iundifdif  32585  fmptco1f1o  32652  gtiso  32712  gsumhashmul  33040  cycpmco2lem4  33122  cycpmconjslem2  33148  qusima  33401  mxidlirred  33465  2sqr3minply  33738  zarcls0  33814  esumpr2  34031  omssubaddlem  34264  eulerpartlemt  34336  ofcccat  34520  2cycld  35106  satfv1lem  35330  topjoin  36331  tailfval  36338  tailf  36341  dvasin  37664  dvacos  37665  opidon2OLD  37814  cdleme4  40195  cdleme22e  40301  cdleme22eALTN  40302  cdleme42a  40428  cdleme42d  40430  cdlemk20  40831  dih1dimatlem0  41285  lcfrlem2  41500  elrfi  42650  fzsplit1nn0  42710  rabdiophlem2  42758  eldioph4b  42767  diophren  42769  pell1qrgaplem  42829  rngunsnply  43130  om2  43366  oe2  43368  disjinfi  45099  fmuldfeq  45504  limciccioolb  45542  ditgeq3d  45885  stoweidlem44  45965  dirkertrigeq  46022  fourierdlem32  46060  fourierdlem33  46061  fourierdlem42  46070  fourierdlem62  46089  fourierdlem84  46111  fourierdlem85  46112  fourierdlem97  46124  fourierdlem98  46125  fourierdlem102  46129  fourierdlem104  46131  fourierdlem113  46140  fourierdlem114  46141  fourierswlem  46151  fouriersw  46152  sssalgen  46256  meadjun  46383  fcoreslem2  46979  fnfocofob  46994  deccarry  47226  fsumsplitsndif  47247  gricushgr  47770  ushggricedg  47780  2sphere  48483  iscnrm3rlem1  48620