Theorem eqtr2di 2812

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr2di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr2di.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtr2di	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2di

Step	Hyp	Ref	Expression
1		eqtr2di.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr2di.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtrdi 2811	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2766	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 2732

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

This theorem is used by:  eqtr4id  2814  csbin  4400  csbif  4540  elpr2elpr  4829  csbuni  4898  csbima12  6075  somincom  6128  resresdm  6229  iotauni2  6505  csbfv12  6923  opabiotafun  6958  fvmptrabfv  7019  fndifnfp  7174  elxp4  7919  elxp5  7920  fo1stres  8012  fo2ndres  8013  sbcoteq1a  8048  eloprabi  8060  fo2ndf  8118  seqomlem2  8440  oev2  8510  odi  8566  fundmen  9038  xpsnen  9059  xpassen  9069  ac6sfi  9254  infeq5  9616  alephsuc3  10589  rankcf  10786  ine0  11673  nn0n0n1ge2  12596  fzval2  13564  fseq1p1m1  13653  fzosplitprm1  13834  hashfun  14502  hashf1  14522  hashtpg  14550  cshword  14862  wrd2pr2op  15014  wrd3tpop  15019  s3rex  15021  relexpsucrd  15106  relexpsucld  15107  sgnmul  15180  fsum2dlem  15856  fprod2dlem  16067  ef4p  16201  sin01bnd  16273  odd2np1  16431  bitsinvp1  16539  smumullem  16582  oppcmon  17827  issubc2  17925  curf1cl  18316  curfcl  18320  cnvtsr  18676  ex-chn1  18725  sylow1lem1  19725  sylow2a  19746  ablsimpgfindlem1  20236  coe1fzgsumdlem  22528  evl1gsumdlem  22581  pmatcollpw3lem  23008  pptbas  23233  2ndcctbss  23681  txcmplem1  23867  qtopeu  23942  alexsubALTlem3  24275  ustuqtop5  24471  psmetdmdm  24531  xmetdmdm  24561  pcopt  25250  pcorevlem  25254  voliunlem1  25778  i1fima2  25907  iblabs  26056  dveflem  26206  deg1val  26321  abssinper  26758  mulcxplem  26921  dvatan  27172  lgamgulmlem2  27266  lgamgulmlem5  27269  lgseisenlem1  27611  dchrisumlem1  27725  pntlemr  27838  negsdi  28315  noseqrdg0  28572  eucliddivs  28641  pw2cut2  28727  krippenlem  29041  prlngmid2  29318  cusgredg  29884  cusgrsizeindb0  29909  numclwlk1lem1  30849  numclwwlk3lem2lem  30863  grporndm  30991  vafval  31084  smfval  31086  hvmul0  31505  cmcmlem  32072  cmbr3i  32081  nmbdfnlbi  32530  nmcfnlbi  32533  nmopcoadji  32582  pjin2i  32674  hst1h  32708  xaddeq0  33224  gsumhashmul  33507  cycpmconjslem1  33594  archirngz  33629  opprqusmulr  33893  dflringlem3  33906  dflring4  33908  selvply1rhm0  34036  esplyfvaln  34084  esplyind  34085  extdgfialglem2  34203  constrinvcl  34283  cos9thpiminplylem1  34292  esumcst  34573  eulerpartlems  34871  dstfrvunirn  34986  subfacp1lem5  35763  cvmliftlem10  35873  fnessref  36976  fnemeet2  36986  poimirlem4  38373  poimirlem19  38388  poimirlem20  38389  poimirlem23  38392  poimirlem24  38393  poimirlem25  38394  poimirlem28  38397  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  itg2addnclem  38420  itg2addnc  38423  iblabsnc  38433  iblmulc2nc  38434  sdclem2  38492  blbnd  38537  ismgmOLD  38600  ismndo2  38624  rnresequniqs  39082  tendo0co2  41661  dvhfvadd  41964  dvh4dimN  42320  mzpcompact2lem  43596  diophrw  43604  eldioph2  43607  pellexlem5  43674  pell1qr1  43712  rmxy0  43764  wessf1ornlem  46017  cncfuni  46714  cncfiooicclem1  46721  dvnprodlem1  46774  fourierdlem38  46973  fourierdlem60  46994  fourierdlem61  46995  fourierdlem79  47013  fourierdlem112  47046  fourierswlem  47058  fouriersw  47059  chnerlem1  47710  fvmptrab  48180  fvmptrabdm  48181  fmtnofac2  48472  nn0sumshdiglem1  49551  eloprab1st2nd  49796  dmdm  49979  isinito2lem  50424  termolmd  50596