Theorem eqtr2id 2778

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 2777	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2736	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  eqtr3di  2780  opeqsng  5466  relop  5817  ordintdif  6386  iotanul  6492  funopg  6553  funcnvres  6597  fpropnf1  7245  csbriota  7362  csbov123  7434  mpocurryd  8251  nneob  8623  sucdom2OLD  9056  sucdom2  9173  unblem2  9247  pwfilem  9274  prfi  9281  pr2ne  9964  kmlem2  10112  kmlem11  10121  kmlem12  10122  cflim3  10222  1idsr  11058  recextlem1  11815  quoremz  13824  quoremnn0ALT  13826  intfrac2  13827  hashprg  14367  hashfacen  14426  leiso  14431  ccatrid  14559  repsw2  14923  repsw3  14924  cvgcmpce  15791  explecnv  15838  risefallfac  15997  ramub1lem1  17004  ressress  17224  subsubc  17822  grp1inv  18987  eqg0subg  19135  psgnunilem1  19430  psgn0fv0  19448  psgnsn  19457  efginvrel2  19664  efgredleme  19680  efgcpbllemb  19692  cmnbascntr  19742  frgpnabllem1  19810  gsumzaddlem  19858  gsumzmhm  19874  fsfnn0gsumfsffz  19920  dprd2da  19981  dpjcntz  19991  dpjdisj  19992  dpjlsm  19993  dpjidcl  19997  ablfac1lem  20007  ablfac1eu  20012  ringurd  20101  funcrngcsetcALT  20557  lmhmlsp  20963  elrspsn  21157  frlmip  21694  opsrtoslem2  21970  mplmon2mul  21983  1marepvmarrepid  22469  m1detdiag  22491  cramerimplem2  22578  pmatcollpw3lem  22677  chpscmatgsumbin  22738  chpscmatgsummon  22739  cayhamlem2  22778  neitr  23074  fixufil  23816  trust  24124  restmetu  24465  nmfval0  24485  nmval2  24487  rerest  24699  xrrest  24703  xrge0gsumle  24729  mpomulcn  24765  rrxip  25297  rrx0  25304  rrxdsfi  25318  voliunlem3  25460  volsup  25464  itg1addlem5  25608  itg2monolem1  25658  itg2cnlem2  25670  itgmpt  25691  iblcnlem1  25696  itgcnlem  25698  itgioo  25724  limcres  25794  mdegfval  25974  dgrlem  26141  coeidlem  26149  mcubic  26764  binom4  26767  dquartlem2  26769  amgm  26908  lgamgulmlem2  26947  eflgam  26962  wilthlem2  26986  rpvmasum2  27430  pntlemo  27525  bday0b  27749  zzs12  28346  wlkres  29605  3wlkond  30107  3cycld  30114  frgrncvvdeqlem3  30237  vc2OLD  30504  nvge0  30609  nmoo0  30727  bcsiALT  31115  pjchi  31368  shjshseli  31429  spanpr  31516  pjinvari  32127  mdslmd1lem2  32262  iundifdifd  32497  iundifdif  32498  fmptco1f1o  32564  gtiso  32631  gsumhashmul  33008  cycpmco2lem4  33093  cycpmconjslem2  33119  qusima  33386  mxidlirred  33450  2sqr3minply  33777  zarcls0  33865  esumpr2  34064  omssubaddlem  34297  eulerpartlemt  34369  ofcccat  34541  2cycld  35132  satfv1lem  35356  topjoin  36360  tailfval  36367  tailf  36370  dvasin  37705  dvacos  37706  opidon2OLD  37855  cdleme4  40239  cdleme22e  40345  cdleme22eALTN  40346  cdleme42a  40472  cdleme42d  40474  cdlemk20  40875  dih1dimatlem0  41329  lcfrlem2  41544  elrfi  42689  fzsplit1nn0  42749  rabdiophlem2  42797  eldioph4b  42806  diophren  42808  pell1qrgaplem  42868  rngunsnply  43165  om2  43400  oe2  43402  disjinfi  45193  fmuldfeq  45588  limciccioolb  45626  ditgeq3d  45969  stoweidlem44  46049  dirkertrigeq  46106  fourierdlem32  46144  fourierdlem33  46145  fourierdlem42  46154  fourierdlem62  46173  fourierdlem84  46195  fourierdlem85  46196  fourierdlem97  46208  fourierdlem98  46209  fourierdlem102  46213  fourierdlem104  46215  fourierdlem113  46224  fourierdlem114  46225  fourierswlem  46235  fouriersw  46236  sssalgen  46340  meadjun  46467  fcoreslem2  47069  fnfocofob  47084  deccarry  47316  fsumsplitsndif  47378  gricushgr  47921  ushggricedg  47931  2sphere  48742  iscnrm3rlem1  48932