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  4395  csbif  4536  elpr2elpr  4823  csbuni  4890  csbima12  6034  somincom  6087  resresdm  6186  iotauni2  6458  csbfv12  6872  opabiotafun  6907  fvmptrabfv  6966  fndifnfp  7116  elxp4  7862  elxp5  7863  fo1stres  7957  fo2ndres  7958  sbcoteq1a  7993  eloprabi  8005  fo2ndf  8061  seqomlem2  8380  oev2  8448  odi  8504  fundmen  8963  xpsnen  8985  xpassen  8995  ac6sfi  9189  infeq5  9552  alephsuc3  10493  rankcf  10690  ine0  11574  nn0n0n1ge2  12471  fzval2  13432  fseq1p1m1  13520  fzosplitprm1  13699  hashfun  14363  hashf1  14383  hashtpg  14411  cshword  14716  wrd2pr2op  14869  wrd3tpop  14874  relexpsucrd  14959  relexpsucld  14960  fsum2dlem  15696  fprod2dlem  15906  ef4p  16041  sin01bnd  16113  odd2np1  16271  bitsinvp1  16379  smumullem  16422  oppcmon  17664  issubc2  17762  curf1cl  18153  curfcl  18157  cnvtsr  18513  sylow1lem1  19496  sylow2a  19517  ablsimpgfindlem1  20007  coe1fzgsumdlem  22207  evl1gsumdlem  22260  pmatcollpw3lem  22687  pptbas  22912  2ndcctbss  23359  txcmplem1  23545  qtopeu  23620  alexsubALTlem3  23953  ustuqtop5  24150  psmetdmdm  24210  xmetdmdm  24240  pcopt  24939  pcorevlem  24943  voliunlem1  25468  i1fima2  25597  iblabs  25747  dveflem  25900  deg1val  26018  abssinper  26447  mulcxplem  26610  dvatan  26862  lgamgulmlem2  26957  lgamgulmlem5  26960  lgseisenlem1  27303  dchrisumlem1  27417  pntlemr  27530  negsdi  27980  noseqrdg0  28225  eucliddivs  28289  krippenlem  28654  cusgredg  29388  cusgrsizeindb0  29414  numclwlk1lem1  30332  numclwwlk3lem2lem  30346  grporndm  30473  vafval  30566  smfval  30568  hvmul0  30987  cmcmlem  31554  cmbr3i  31563  nmbdfnlbi  32012  nmcfnlbi  32015  nmopcoadji  32064  pjin2i  32156  hst1h  32190  xaddeq0  32715  sgnmul  32799  gsumhashmul  33033  cycpmconjslem1  33115  archirngz  33150  opprqusmulr  33447  extdgfialglem2  33679  constrinvcl  33759  cos9thpiminplylem1  33768  esumcst  34049  eulerpartlems  34347  dstfrvunirn  34462  subfacp1lem5  35176  cvmliftlem10  35286  fnessref  36350  fnemeet2  36360  poimirlem4  37623  poimirlem19  37638  poimirlem20  37639  poimirlem23  37642  poimirlem24  37643  poimirlem25  37644  poimirlem28  37647  ovoliunnfl  37661  voliunnfl  37663  volsupnfl  37664  itg2addnclem  37670  itg2addnc  37673  iblabsnc  37683  iblmulc2nc  37684  sdclem2  37741  blbnd  37786  ismgmOLD  37849  ismndo2  37873  rnresequniqs  38321  tendo0co2  40787  dvhfvadd  41090  dvh4dimN  41446  mzpcompact2lem  42744  diophrw  42752  eldioph2  42755  pellexlem5  42826  pell1qr1  42864  rmxy0  42916  wessf1ornlem  45183  cncfuni  45887  cncfiooicclem1  45894  dvnprodlem1  45947  fourierdlem38  46146  fourierdlem60  46167  fourierdlem61  46168  fourierdlem79  46186  fourierdlem112  46219  fourierswlem  46231  fouriersw  46232  fvmptrab  47296  fvmptrabdm  47297  fmtnofac2  47573  nn0sumshdiglem1  48626  eloprab1st2nd  48872  dmdm  49058  isinito2lem  49503  termolmd  49675