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 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  eqtr4id  2814  csbin  4399  csbif  4539  elpr2elpr  4823  csbuni  4897  csbima12  6078  somincom  6130  resresdm  6237  iotauni2  6513  csbfv12  6935  opabiotafun  6970  fvmptrabfv  7031  fndifnfp  7185  elxp4  7938  elxp5  7939  fo1stres  8031  fo2ndres  8032  sbcoteq1a  8066  eloprabi  8078  fo2ndf  8138  seqomlem2  8468  oev2  8538  odi  8594  fundmen  9066  xpsnen  9087  xpassen  9097  ac6sfi  9282  infeq5  9645  alephsuc3  10672  rankcf  10869  ine0  11758  nn0n0n1ge2  12681  fzval2  13649  fseq1p1m1  13739  fzosplitprm1  13920  hashfun  14589  hashf1  14609  hashtpg  14637  cshword  14950  wrd2pr2op  15103  wrd3tpop  15108  s3rex  15110  relexpsucrd  15195  relexpsucld  15196  sgnmul  15269  fsum2dlem  15945  fprod2dlem  16156  ef4p  16290  sin01bnd  16362  odd2np1  16520  bitsinvp1  16628  smumullem  16671  oppcmon  17922  issubc2  18020  curf1cl  18411  curfcl  18415  cnvtsr  18771  ex-chn1  18820  sylow1lem1  19821  sylow2a  19842  ablsimpgfindlem1  20332  coe1fzgsumdlem  22630  evl1gsumdlem  22683  pmatcollpw3lem  23110  pptbas  23335  2ndcctbss  23783  txcmplem1  23969  qtopeu  24044  alexsubALTlem3  24377  ustuqtop5  24573  psmetdmdm  24633  xmetdmdm  24663  pcopt  25352  pcorevlem  25356  voliunlem1  25880  i1fima2  26009  iblabs  26158  dveflem  26308  deg1val  26423  abssinper  26858  mulcxplem  27021  dvatan  27272  lgamgulmlem2  27366  lgamgulmlem5  27369  lgseisenlem1  27711  dchrisumlem1  27825  pntlemr  27938  negsdi  28445  noseqrdg0  28702  eucliddivs  28771  pw2cut2  28857  krippenlem  29171  prlngmid2  29448  cusgredg  30014  cusgrsizeindb0  30039  numclwlk1lem1  30979  numclwwlk3lem2lem  30993  grporndm  31121  vafval  31214  smfval  31216  hvmul0  31635  cmcmlem  32202  cmbr3i  32211  nmbdfnlbi  32660  nmcfnlbi  32663  nmopcoadji  32712  pjin2i  32804  hst1h  32838  xaddeq0  33395  gsumhashmul  33678  cycpmconjslem1  33765  archirngz  33800  opprqusmulr  34065  dflringlem3  34078  dflring4  34080  selvply1rhm0  34208  esplyfvaln  34256  esplyind  34257  extdgfialglem2  34375  constrinvcl  34455  cos9thpiminplylem1  34464  esumcst  34745  eulerpartlems  35042  dstfrvunirn  35157  subfacp1lem5  36039  cvmliftlem10  36149  fnessref  37241  fnemeet2  37251  poimirlem4  38651  poimirlem19  38666  poimirlem20  38667  poimirlem23  38670  poimirlem24  38671  poimirlem25  38672  poimirlem28  38675  ovoliunnfl  38689  voliunnfl  38691  volsupnfl  38692  itg2addnclem  38698  itg2addnc  38701  iblabsnc  38711  iblmulc2nc  38712  sdclem2  38785  blbnd  38830  ismgmOLD  38893  ismndo2  38917  rnresequniqs  39375  tendo0co2  41954  dvhfvadd  42257  dvh4dimN  42613  mzpcompact2lem  43871  diophrw  43879  eldioph2  43882  pellexlem5  43949  pell1qr1  43987  rmxy0  44039  wessf1ornlem  46308  cncfuni  47004  cncfiooicclem1  47011  dvnprodlem1  47064  fourierdlem38  47263  fourierdlem60  47284  fourierdlem61  47285  fourierdlem79  47303  fourierdlem112  47336  fourierswlem  47348  fouriersw  47349  chnerlem1  48000  fvmptrab  48470  fvmptrabdm  48471  fmtnofac2  48762  nn0sumshdiglem1  49841  eloprab1st2nd  50087  dmdm  50275  isinito2lem  50741  termolmd  50961