Theorem eqtr2di 2781

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqtr4id  2783  csbin  4401  csbif  4542  elpr2elpr  4829  csbuni  4896  csbima12  6039  somincom  6095  resresdm  6194  iotauni2  6468  csbfv12  6888  opabiotafun  6923  fvmptrabfv  6982  fndifnfp  7132  elxp4  7878  elxp5  7879  fo1stres  7973  fo2ndres  7974  sbcoteq1a  8009  eloprabi  8021  fo2ndf  8077  seqomlem2  8396  oev2  8464  odi  8520  fundmen  8979  xpsnen  9002  xpassen  9012  ac6sfi  9207  infeq5  9566  alephsuc3  10509  rankcf  10706  ine0  11589  nn0n0n1ge2  12486  fzval2  13447  fseq1p1m1  13535  fzosplitprm1  13714  hashfun  14378  hashf1  14398  hashtpg  14426  cshword  14732  wrd2pr2op  14885  wrd3tpop  14890  relexpsucrd  14975  relexpsucld  14976  fsum2dlem  15712  fprod2dlem  15922  ef4p  16057  sin01bnd  16129  odd2np1  16287  bitsinvp1  16395  smumullem  16438  oppcmon  17676  issubc2  17774  curf1cl  18165  curfcl  18169  cnvtsr  18523  sylow1lem1  19504  sylow2a  19525  ablsimpgfindlem1  20015  coe1fzgsumdlem  22166  evl1gsumdlem  22219  pmatcollpw3lem  22646  pptbas  22871  2ndcctbss  23318  txcmplem1  23504  qtopeu  23579  alexsubALTlem3  23912  ustuqtop5  24109  psmetdmdm  24169  xmetdmdm  24199  pcopt  24898  pcorevlem  24902  voliunlem1  25427  i1fima2  25556  iblabs  25706  dveflem  25859  deg1val  25977  abssinper  26406  mulcxplem  26569  dvatan  26821  lgamgulmlem2  26916  lgamgulmlem5  26919  lgseisenlem1  27262  dchrisumlem1  27376  pntlemr  27489  negsdi  27932  noseqrdg0  28177  eucliddivs  28241  krippenlem  28593  cusgredg  29327  cusgrsizeindb0  29353  numclwlk1lem1  30271  numclwwlk3lem2lem  30285  grporndm  30412  vafval  30505  smfval  30507  hvmul0  30926  cmcmlem  31493  cmbr3i  31502  nmbdfnlbi  31951  nmcfnlbi  31954  nmopcoadji  32003  pjin2i  32095  hst1h  32129  xaddeq0  32649  sgnmul  32733  gsumhashmul  32974  cycpmconjslem1  33084  archirngz  33116  opprqusmulr  33435  constrinvcl  33736  cos9thpiminplylem1  33745  esumcst  34026  eulerpartlems  34324  dstfrvunirn  34439  subfacp1lem5  35144  cvmliftlem10  35254  fnessref  36318  fnemeet2  36328  poimirlem4  37591  poimirlem19  37606  poimirlem20  37607  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem28  37615  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  itg2addnclem  37638  itg2addnc  37641  iblabsnc  37651  iblmulc2nc  37652  sdclem2  37709  blbnd  37754  ismgmOLD  37817  ismndo2  37841  rnresequniqs  38289  tendo0co2  40755  dvhfvadd  41058  dvh4dimN  41414  mzpcompact2lem  42712  diophrw  42720  eldioph2  42723  pellexlem5  42794  pell1qr1  42832  rmxy0  42885  wessf1ornlem  45152  cncfuni  45857  cncfiooicclem1  45864  dvnprodlem1  45917  fourierdlem38  46116  fourierdlem60  46137  fourierdlem61  46138  fourierdlem79  46156  fourierdlem112  46189  fourierswlem  46201  fouriersw  46202  fvmptrab  47266  fvmptrabdm  47267  fmtnofac2  47543  nn0sumshdiglem1  48583  eloprab1st2nd  48829  dmdm  49015  isinito2lem  49460  termolmd  49632