Theorem eqtr2di 2789

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqtr4id  2791  csbin  4396  csbif  4539  elpr2elpr  4827  csbuni  4895  csbima12  6046  somincom  6099  resresdm  6199  iotauni2  6472  csbfv12  6887  opabiotafun  6922  fvmptrabfv  6982  fndifnfp  7132  elxp4  7874  elxp5  7875  fo1stres  7969  fo2ndres  7970  sbcoteq1a  8005  eloprabi  8017  fo2ndf  8073  seqomlem2  8392  oev2  8460  odi  8516  fundmen  8980  xpsnen  9001  xpassen  9011  ac6sfi  9196  infeq5  9558  alephsuc3  10503  rankcf  10700  ine0  11584  nn0n0n1ge2  12481  fzval2  13438  fseq1p1m1  13526  fzosplitprm1  13706  hashfun  14372  hashf1  14392  hashtpg  14420  cshword  14726  wrd2pr2op  14878  wrd3tpop  14883  relexpsucrd  14968  relexpsucld  14969  fsum2dlem  15705  fprod2dlem  15915  ef4p  16050  sin01bnd  16122  odd2np1  16280  bitsinvp1  16388  smumullem  16431  oppcmon  17674  issubc2  17772  curf1cl  18163  curfcl  18167  cnvtsr  18523  ex-chn1  18572  sylow1lem1  19539  sylow2a  19560  ablsimpgfindlem1  20050  coe1fzgsumdlem  22259  evl1gsumdlem  22312  pmatcollpw3lem  22739  pptbas  22964  2ndcctbss  23411  txcmplem1  23597  qtopeu  23672  alexsubALTlem3  24005  ustuqtop5  24201  psmetdmdm  24261  xmetdmdm  24291  pcopt  24990  pcorevlem  24994  voliunlem1  25519  i1fima2  25648  iblabs  25798  dveflem  25951  deg1val  26069  abssinper  26498  mulcxplem  26661  dvatan  26913  lgamgulmlem2  27008  lgamgulmlem5  27011  lgseisenlem1  27354  dchrisumlem1  27468  pntlemr  27581  negsdi  28058  noseqrdg0  28315  eucliddivs  28384  pw2cut2  28470  krippenlem  28774  cusgredg  29509  cusgrsizeindb0  29535  numclwlk1lem1  30456  numclwwlk3lem2lem  30470  grporndm  30598  vafval  30691  smfval  30693  hvmul0  31112  cmcmlem  31679  cmbr3i  31688  nmbdfnlbi  32137  nmcfnlbi  32140  nmopcoadji  32189  pjin2i  32281  hst1h  32315  xaddeq0  32844  sgnmul  32927  gsumhashmul  33161  cycpmconjslem1  33248  archirngz  33283  opprqusmulr  33584  esplyfvaln  33751  esplyind  33752  extdgfialglem2  33871  constrinvcl  33951  cos9thpiminplylem1  33960  esumcst  34241  eulerpartlems  34538  dstfrvunirn  34653  subfacp1lem5  35400  cvmliftlem10  35510  fnessref  36573  fnemeet2  36583  poimirlem4  37875  poimirlem19  37890  poimirlem20  37891  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem28  37899  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  itg2addnclem  37922  itg2addnc  37925  iblabsnc  37935  iblmulc2nc  37936  sdclem2  37993  blbnd  38038  ismgmOLD  38101  ismndo2  38125  rnresequniqs  38585  tendo0co2  41164  dvhfvadd  41467  dvh4dimN  41823  mzpcompact2lem  43108  diophrw  43116  eldioph2  43119  pellexlem5  43190  pell1qr1  43228  rmxy0  43280  wessf1ornlem  45544  cncfuni  46244  cncfiooicclem1  46251  dvnprodlem1  46304  fourierdlem38  46503  fourierdlem60  46524  fourierdlem61  46525  fourierdlem79  46543  fourierdlem112  46576  fourierswlem  46588  fouriersw  46589  chnerlem1  47240  fvmptrab  47652  fvmptrabdm  47653  fmtnofac2  47929  nn0sumshdiglem1  48981  eloprab1st2nd  49227  dmdm  49412  isinito2lem  49857  termolmd  50029