Theorem eqtr2id 2779

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqtr3di  2781  opeqsng  5443  relop  5790  ordintdif  6357  iotanul  6461  funopg  6515  funcnvres  6559  fpropnf1  7201  csbriota  7318  csbov123  7390  mpocurryd  8199  nneob  8571  sucdom2  9112  unblem2  9177  pwfilem  9202  prfi  9208  pr2ne  9896  kmlem2  10043  kmlem11  10052  kmlem12  10053  cflim3  10153  1idsr  10989  recextlem1  11747  quoremz  13759  quoremnn0ALT  13761  intfrac2  13762  hashprg  14302  hashfacen  14361  leiso  14366  ccatrid  14495  repsw2  14857  repsw3  14858  cvgcmpce  15725  explecnv  15772  risefallfac  15931  ramub1lem1  16938  ressress  17158  subsubc  17760  chnfi  18540  grp1inv  18961  eqg0subg  19109  psgnunilem1  19406  psgn0fv0  19424  psgnsn  19433  efginvrel2  19640  efgredleme  19656  efgcpbllemb  19668  cmnbascntr  19718  frgpnabllem1  19786  gsumzaddlem  19834  gsumzmhm  19850  fsfnn0gsumfsffz  19896  dprd2da  19957  dpjcntz  19967  dpjdisj  19968  dpjlsm  19969  dpjidcl  19973  ablfac1lem  19983  ablfac1eu  19988  ringurd  20104  funcrngcsetcALT  20557  lmhmlsp  20984  elrspsn  21178  frlmip  21716  opsrtoslem2  21992  mplmon2mul  22005  1marepvmarrepid  22491  m1detdiag  22513  cramerimplem2  22600  pmatcollpw3lem  22699  chpscmatgsumbin  22760  chpscmatgsummon  22761  cayhamlem2  22800  neitr  23096  fixufil  23838  trust  24145  restmetu  24486  nmfval0  24506  nmval2  24508  rerest  24720  xrrest  24724  xrge0gsumle  24750  mpomulcn  24786  rrxip  25318  rrx0  25325  rrxdsfi  25339  voliunlem3  25481  volsup  25485  itg1addlem5  25629  itg2monolem1  25679  itg2cnlem2  25691  itgmpt  25712  iblcnlem1  25717  itgcnlem  25719  itgioo  25745  limcres  25815  mdegfval  25995  dgrlem  26162  coeidlem  26170  mcubic  26785  binom4  26788  dquartlem2  26790  amgm  26929  lgamgulmlem2  26968  eflgam  26983  wilthlem2  27007  rpvmasum2  27451  pntlemo  27546  bday0b  27775  pw2cut2  28383  zzs12  28386  wlkres  29648  3wlkond  30149  3cycld  30156  frgrncvvdeqlem3  30279  vc2OLD  30546  nvge0  30651  nmoo0  30769  bcsiALT  31157  pjchi  31410  shjshseli  31471  spanpr  31558  pjinvari  32169  mdslmd1lem2  32304  iundifdifd  32539  iundifdif  32540  fmptco1f1o  32613  gtiso  32680  gsumhashmul  33039  cycpmco2lem4  33096  cycpmconjslem2  33122  qusima  33371  mxidlirred  33435  extdgfialglem1  33703  2sqr3minply  33791  zarcls0  33879  esumpr2  34078  omssubaddlem  34310  eulerpartlemt  34382  ofcccat  34554  2cycld  35180  satfv1lem  35404  topjoin  36405  tailfval  36412  tailf  36415  dvasin  37750  dvacos  37751  opidon2OLD  37900  cdleme4  40283  cdleme22e  40389  cdleme22eALTN  40390  cdleme42a  40516  cdleme42d  40518  cdlemk20  40919  dih1dimatlem0  41373  lcfrlem2  41588  elrfi  42733  fzsplit1nn0  42793  rabdiophlem2  42841  eldioph4b  42850  diophren  42852  pell1qrgaplem  42912  rngunsnply  43208  om2  43443  oe2  43445  disjinfi  45235  fmuldfeq  45629  limciccioolb  45667  ditgeq3d  46008  stoweidlem44  46088  dirkertrigeq  46145  fourierdlem32  46183  fourierdlem33  46184  fourierdlem42  46193  fourierdlem62  46212  fourierdlem84  46234  fourierdlem85  46235  fourierdlem97  46247  fourierdlem98  46248  fourierdlem102  46252  fourierdlem104  46254  fourierdlem113  46263  fourierdlem114  46264  fourierswlem  46274  fouriersw  46275  sssalgen  46379  meadjun  46506  fcoreslem2  47101  fnfocofob  47116  deccarry  47348  fsumsplitsndif  47410  gricushgr  47954  ushggricedg  47964  2sphere  48787  iscnrm3rlem1  48977