Theorem eqtr2id 2810

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 2809	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2768	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 2155  ax-ext 2734

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

This theorem is used by:  eqtr3di  2812  opeqsng  5484  relop  5834  ordintdif  6413  iotanul  6517  funopg  6571  funcnvres  6615  fpropnf1  7268  csbriota  7389  csbov123  7461  mpocurryd  8271  om2  8577  nneob  8648  sucdom2  9201  unblem2  9267  pwfilem  9291  prfi  9297  pr2ne  10012  kmlem2  10158  kmlem11  10167  kmlem12  10168  cflim3  10268  1idsr  11111  recextlem1  11872  quoremz  13920  quoremnn0ALT  13922  intfrac2  13923  hashprg  14463  hashfacen  14523  leiso  14528  ccatrid  14657  repsw2  15027  repsw3  15028  cvgcmpce  15909  explecnv  15958  risefallfac  16117  ramub1lem1  17124  ressress  17345  subsubc  17948  chnfi  18728  grp1inv  19177  eqg0subg  19330  psgnunilem1  19626  psgn0fv0  19644  psgnsn  19653  efginvrel2  19860  efgredleme  19876  efgcpbllemb  19888  cmnbascntr  19938  frgpnabllem1  20006  gsumzaddlem  20054  gsumzmhm  20070  fsfnn0gsumfsffz  20116  dprd2da  20177  dpjcntz  20187  dpjdisj  20188  dpjlsm  20189  dpjidcl  20193  ablfac1lem  20203  ablfac1eu  20208  ringurd  20330  funcrngcsetcALT  20809  lmhmlsp  21239  elrspsn  21440  frlmip  21997  opsrtoslem2  22278  mplmon2mul  22291  1marepvmarrepid  22803  m1detdiag  22825  cramerimplem2  22915  pmatcollpw3lem  23014  chpscmatgsumbin  23075  chpscmatgsummon  23076  cayhamlem2  23115  neitr  23411  fixufil  24154  trust  24461  restmetu  24802  nmfval0  24822  nmval2  24824  rerest  25036  xrrest  25040  xrge0gsumle  25066  mpomulcn  25101  rrxip  25624  rrx0  25631  rrxdsfi  25645  voliunlem3  25786  volsup  25790  itg1addlem5  25934  itg2monolem1  25984  itg2cnlem2  25996  itgmpt  26017  iblcnlem1  26022  itgcnlem  26024  itgioo  26050  limcres  26120  mdegfval  26294  dgrlem  26462  coeidlem  26470  mcubic  27092  binom4  27095  dquartlem2  27097  amgm  27235  lgamgulmlem2  27274  eflgam  27289  wilthlem2  27313  rpvmasum2  27756  pntlemo  27851  bday0b  28086  pw2cut2  28735  zz12s  28748  wlkres  30136  2cycld  30632  3wlkond  30659  3cycld  30666  frgrncvvdeqlem3  30789  vc2OLD  31057  nvge0  31162  nmoo0  31280  bcsiALT  31668  pjchi  31921  shjshseli  31982  spanpr  32069  pjinvari  32680  mdslmd1lem2  32815  iundifdifd  33043  iundifdif  33044  fresunsn  33106  fmptco1f1o  33114  gtiso  33181  gsumhashmul  33515  cycpmco2lem4  33577  cycpmconjslem2  33603  qusima  33845  mxidlirred  33883  selvascl  34035  esplyind  34093  vietalem  34097  extdgfialglem1  34210  2sqr3minply  34298  zarcls0  34386  esumpr2  34585  omssubaddlem  34818  eulerpartlemt  34890  ofcccat  35062  satfv1lem  35949  topjoin  36992  tailfval  36999  tailf  37002  dvasin  38461  dvacos  38462  opidon2OLD  38612  cdleme4  41119  cdleme22e  41225  cdleme22eALTN  41226  cdleme42a  41352  cdleme42d  41354  cdlemk20  41755  dih1dimatlem0  42209  lcfrlem2  42424  elrfi  43547  fzsplit1nn0  43607  rabdiophlem2  43651  eldioph4b  43660  diophren  43662  pell1qrgaplem  43722  rngunsnply  44018  oe2  44254  disjinfi  46032  fmuldfeq  46421  limciccioolb  46459  ditgeq3d  46800  stoweidlem44  46880  dirkertrigeq  46937  fourierdlem32  46975  fourierdlem33  46976  fourierdlem42  46985  fourierdlem62  47004  fourierdlem84  47026  fourierdlem85  47027  fourierdlem97  47039  fourierdlem98  47040  fourierdlem102  47044  fourierdlem104  47046  fourierdlem113  47055  fourierdlem114  47056  fourierswlem  47066  fouriersw  47067  sssalgen  47171  meadjun  47298  cos3t  47744  sin5tlem1  47745  fcoreslem2  47960  fnfocofob  47975  deccarry  48207  fsumsplitsndif  48277  gricushgr  48841  ushggricedg  48851  2sphere  49687  iscnrm3rlem1  49874