Theorem eqtr2id 2814

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  eqtr3di  2816  opeqsng  5491  relop  5841  ordintdif  6419  iotanul  6523  funopg  6577  funcnvres  6621  fpropnf1  7272  csbriota  7395  csbov123  7467  mpocurryd  8274  om2  8580  nneob  8651  sucdom2  9197  unblem2  9263  pwfilem  9287  prfi  9293  pr2ne  10008  kmlem2  10154  kmlem11  10163  kmlem12  10164  cflim3  10264  1idsr  11101  recextlem1  11862  quoremz  13908  quoremnn0ALT  13910  intfrac2  13911  hashprg  14451  hashfacen  14511  leiso  14516  ccatrid  14645  repsw2  15013  repsw3  15014  cvgcmpce  15896  explecnv  15945  risefallfac  16104  ramub1lem1  17111  ressress  17332  subsubc  17935  chnfi  18715  grp1inv  19145  eqg0subg  19298  psgnunilem1  19594  psgn0fv0  19612  psgnsn  19621  efginvrel2  19828  efgredleme  19844  efgcpbllemb  19856  cmnbascntr  19906  frgpnabllem1  19974  gsumzaddlem  20022  gsumzmhm  20038  fsfnn0gsumfsffz  20084  dprd2da  20145  dpjcntz  20155  dpjdisj  20156  dpjlsm  20157  dpjidcl  20161  ablfac1lem  20171  ablfac1eu  20176  ringurd  20298  funcrngcsetcALT  20777  lmhmlsp  21207  elrspsn  21408  frlmip  21965  opsrtoslem2  22244  mplmon2mul  22257  1marepvmarrepid  22769  m1detdiag  22791  cramerimplem2  22878  pmatcollpw3lem  22977  chpscmatgsumbin  23038  chpscmatgsummon  23039  cayhamlem2  23078  neitr  23374  fixufil  24116  trust  24423  restmetu  24764  nmfval0  24784  nmval2  24786  rerest  24998  xrrest  25002  xrge0gsumle  25028  mpomulcn  25063  rrxip  25586  rrx0  25593  rrxdsfi  25607  voliunlem3  25748  volsup  25752  itg1addlem5  25896  itg2monolem1  25946  itg2cnlem2  25958  itgmpt  25979  iblcnlem1  25984  itgcnlem  25986  itgioo  26012  limcres  26082  mdegfval  26256  dgrlem  26423  coeidlem  26431  mcubic  27049  binom4  27052  dquartlem2  27054  amgm  27192  lgamgulmlem2  27231  eflgam  27246  wilthlem2  27270  rpvmasum2  27713  pntlemo  27808  bday0b  28043  pw2cut2  28692  zz12s  28705  wlkres  30055  3wlkond  30559  3cycld  30566  frgrncvvdeqlem3  30689  vc2OLD  30957  nvge0  31062  nmoo0  31180  bcsiALT  31568  pjchi  31821  shjshseli  31882  spanpr  31969  pjinvari  32580  mdslmd1lem2  32715  iundifdifd  32943  iundifdif  32944  fresunsn  33007  fmptco1f1o  33015  gtiso  33083  gsumhashmul  33418  cycpmco2lem4  33480  cycpmconjslem2  33506  qusima  33748  mxidlirred  33786  selvascl  33938  esplyind  33996  vietalem  34000  extdgfialglem1  34113  2sqr3minply  34201  zarcls0  34289  esumpr2  34488  omssubaddlem  34721  eulerpartlemt  34793  ofcccat  34965  2cycld  35651  satfv1lem  35875  topjoin  36917  tailfval  36924  tailf  36927  dvasin  38396  dvacos  38397  opidon2OLD  38546  cdleme4  41053  cdleme22e  41159  cdleme22eALTN  41160  cdleme42a  41286  cdleme42d  41288  cdlemk20  41689  dih1dimatlem0  42143  lcfrlem2  42358  elrfi  43466  fzsplit1nn0  43526  rabdiophlem2  43570  eldioph4b  43579  diophren  43581  pell1qrgaplem  43641  rngunsnply  43937  oe2  44173  disjinfi  45951  fmuldfeq  46340  limciccioolb  46378  ditgeq3d  46719  stoweidlem44  46799  dirkertrigeq  46856  fourierdlem32  46894  fourierdlem33  46895  fourierdlem42  46904  fourierdlem62  46923  fourierdlem84  46945  fourierdlem85  46946  fourierdlem97  46958  fourierdlem98  46959  fourierdlem102  46963  fourierdlem104  46965  fourierdlem113  46974  fourierdlem114  46975  fourierswlem  46985  fouriersw  46986  sssalgen  47090  meadjun  47217  cos3t  47650  sin5tlem1  47651  fcoreslem2  47842  fnfocofob  47857  deccarry  48089  fsumsplitsndif  48159  gricushgr  48723  ushggricedg  48733  2sphere  49570  iscnrm3rlem1  49759