Theorem eqtr2id 2788

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  eqtr3di  2790  opeqsng  5451  relop  5799  ordintdif  6368  iotanul  6472  funopg  6526  funcnvres  6570  fpropnf1  7218  csbriota  7335  csbov123  7407  mpocurryd  8216  om2  8518  nneob  8589  sucdom2  9134  unblem2  9200  pwfilem  9225  prfi  9231  pr2ne  9925  kmlem2  10072  kmlem11  10081  kmlem12  10082  cflim3  10182  1idsr  11019  recextlem1  11778  quoremz  13812  quoremnn0ALT  13814  intfrac2  13815  hashprg  14355  hashfacen  14414  leiso  14419  ccatrid  14548  repsw2  14910  repsw3  14911  cvgcmpce  15779  explecnv  15828  risefallfac  15987  ramub1lem1  16995  ressress  17215  subsubc  17818  chnfi  18598  grp1inv  19022  eqg0subg  19169  psgnunilem1  19466  psgn0fv0  19484  psgnsn  19493  efginvrel2  19700  efgredleme  19716  efgcpbllemb  19728  cmnbascntr  19778  frgpnabllem1  19846  gsumzaddlem  19894  gsumzmhm  19910  fsfnn0gsumfsffz  19956  dprd2da  20017  dpjcntz  20027  dpjdisj  20028  dpjlsm  20029  dpjidcl  20033  ablfac1lem  20043  ablfac1eu  20048  ringurd  20164  funcrngcsetcALT  20620  lmhmlsp  21046  elrspsn  21240  frlmip  21760  opsrtoslem2  22039  mplmon2mul  22052  1marepvmarrepid  22565  m1detdiag  22587  cramerimplem2  22674  pmatcollpw3lem  22773  chpscmatgsumbin  22834  chpscmatgsummon  22835  cayhamlem2  22874  neitr  23170  fixufil  23912  trust  24219  restmetu  24560  nmfval0  24580  nmval2  24582  rerest  24794  xrrest  24798  xrge0gsumle  24824  mpomulcn  24859  rrxip  25382  rrx0  25389  rrxdsfi  25403  voliunlem3  25544  volsup  25548  itg1addlem5  25692  itg2monolem1  25742  itg2cnlem2  25754  itgmpt  25775  iblcnlem1  25780  itgcnlem  25782  itgioo  25808  limcres  25878  mdegfval  26052  dgrlem  26219  coeidlem  26227  mcubic  26836  binom4  26839  dquartlem2  26841  amgm  26979  lgamgulmlem2  27018  eflgam  27033  wilthlem2  27057  rpvmasum2  27500  pntlemo  27595  bday0b  27830  pw2cut2  28479  zz12s  28492  wlkres  29762  3wlkond  30266  3cycld  30273  frgrncvvdeqlem3  30396  vc2OLD  30664  nvge0  30769  nmoo0  30887  bcsiALT  31275  pjchi  31528  shjshseli  31589  spanpr  31676  pjinvari  32287  mdslmd1lem2  32422  iundifdifd  32657  iundifdif  32658  fmptco1f1o  32732  gtiso  32800  gsumhashmul  33155  cycpmco2lem4  33217  cycpmconjslem2  33243  qusima  33498  mxidlirred  33562  selvascl  33708  esplyind  33766  vietalem  33770  extdgfialglem1  33883  2sqr3minply  33971  zarcls0  34059  esumpr2  34258  omssubaddlem  34490  eulerpartlemt  34562  ofcccat  34734  2cycld  35373  satfv1lem  35597  topjoin  36600  tailfval  36607  tailf  36610  dvasin  38078  dvacos  38079  opidon2OLD  38228  cdleme4  40737  cdleme22e  40843  cdleme22eALTN  40844  cdleme42a  40970  cdleme42d  40972  cdlemk20  41373  dih1dimatlem0  41827  lcfrlem2  42042  elrfi  43150  fzsplit1nn0  43210  rabdiophlem2  43254  eldioph4b  43263  diophren  43265  pell1qrgaplem  43325  rngunsnply  43621  oe2  43857  disjinfi  45646  fmuldfeq  46035  limciccioolb  46073  ditgeq3d  46414  stoweidlem44  46494  dirkertrigeq  46551  fourierdlem32  46589  fourierdlem33  46590  fourierdlem42  46599  fourierdlem62  46618  fourierdlem84  46640  fourierdlem85  46641  fourierdlem97  46653  fourierdlem98  46654  fourierdlem102  46658  fourierdlem104  46660  fourierdlem113  46669  fourierdlem114  46670  fourierswlem  46680  fouriersw  46681  sssalgen  46785  meadjun  46912  cos3t  47342  sin5tlem1  47343  fcoreslem2  47534  fnfocofob  47549  deccarry  47781  fsumsplitsndif  47851  gricushgr  48415  ushggricedg  48425  2sphere  49247  iscnrm3rlem1  49437