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  4405  csbif  4546  elpr2elpr  4833  csbuni  4900  csbima12  6050  somincom  6107  resresdm  6206  iotauni2  6480  csbfv12  6906  opabiotafun  6941  fvmptrabfv  7000  fndifnfp  7150  elxp4  7898  elxp5  7899  fo1stres  7994  fo2ndres  7995  sbcoteq1a  8030  eloprabi  8042  fo2ndf  8100  seqomlem2  8419  oev2  8487  odi  8543  fundmen  9002  xpsnen  9025  xpassen  9035  ac6sfi  9231  infeq5  9590  alephsuc3  10533  rankcf  10730  ine0  11613  nn0n0n1ge2  12510  fzval2  13471  fseq1p1m1  13559  fzosplitprm1  13738  hashfun  14402  hashf1  14422  hashtpg  14450  cshword  14756  wrd2pr2op  14909  wrd3tpop  14914  relexpsucrd  14999  relexpsucld  15000  fsum2dlem  15736  fprod2dlem  15946  ef4p  16081  sin01bnd  16153  odd2np1  16311  bitsinvp1  16419  smumullem  16462  oppcmon  17700  issubc2  17798  curf1cl  18189  curfcl  18193  cnvtsr  18547  sylow1lem1  19528  sylow2a  19549  ablsimpgfindlem1  20039  coe1fzgsumdlem  22190  evl1gsumdlem  22243  pmatcollpw3lem  22670  pptbas  22895  2ndcctbss  23342  txcmplem1  23528  qtopeu  23603  alexsubALTlem3  23936  ustuqtop5  24133  psmetdmdm  24193  xmetdmdm  24223  pcopt  24922  pcorevlem  24926  voliunlem1  25451  i1fima2  25580  iblabs  25730  dveflem  25883  deg1val  26001  abssinper  26430  mulcxplem  26593  dvatan  26845  lgamgulmlem2  26940  lgamgulmlem5  26943  lgseisenlem1  27286  dchrisumlem1  27400  pntlemr  27513  negsdi  27956  noseqrdg0  28201  eucliddivs  28265  krippenlem  28617  cusgredg  29351  cusgrsizeindb0  29377  numclwlk1lem1  30298  numclwwlk3lem2lem  30312  grporndm  30439  vafval  30532  smfval  30534  hvmul0  30953  cmcmlem  31520  cmbr3i  31529  nmbdfnlbi  31978  nmcfnlbi  31981  nmopcoadji  32030  pjin2i  32122  hst1h  32156  xaddeq0  32676  sgnmul  32760  gsumhashmul  33001  cycpmconjslem1  33111  archirngz  33143  opprqusmulr  33462  constrinvcl  33763  cos9thpiminplylem1  33772  esumcst  34053  eulerpartlems  34351  dstfrvunirn  34466  subfacp1lem5  35171  cvmliftlem10  35281  fnessref  36345  fnemeet2  36355  poimirlem4  37618  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem28  37642  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem  37665  itg2addnc  37668  iblabsnc  37678  iblmulc2nc  37679  sdclem2  37736  blbnd  37781  ismgmOLD  37844  ismndo2  37868  rnresequniqs  38316  tendo0co2  40782  dvhfvadd  41085  dvh4dimN  41441  mzpcompact2lem  42739  diophrw  42747  eldioph2  42750  pellexlem5  42821  pell1qr1  42859  rmxy0  42912  wessf1ornlem  45179  cncfuni  45884  cncfiooicclem1  45891  dvnprodlem1  45944  fourierdlem38  46143  fourierdlem60  46164  fourierdlem61  46165  fourierdlem79  46183  fourierdlem112  46216  fourierswlem  46228  fouriersw  46229  fvmptrab  47293  fvmptrabdm  47294  fmtnofac2  47570  nn0sumshdiglem1  48610  eloprab1st2nd  48856  dmdm  49042  isinito2lem  49487  termolmd  49659