Theorem eqtr2di 2785

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  eqtr4id  2787  csbin  4391  csbif  4534  elpr2elpr  4822  csbuni  4890  csbima12  6035  somincom  6088  resresdm  6188  iotauni2  6461  csbfv12  6876  opabiotafun  6911  fvmptrabfv  6970  fndifnfp  7119  elxp4  7861  elxp5  7862  fo1stres  7956  fo2ndres  7957  sbcoteq1a  7992  eloprabi  8004  fo2ndf  8060  seqomlem2  8379  oev2  8447  odi  8503  fundmen  8964  xpsnen  8985  xpassen  8995  ac6sfi  9179  infeq5  9538  alephsuc3  10482  rankcf  10679  ine0  11563  nn0n0n1ge2  12460  fzval2  13417  fseq1p1m1  13505  fzosplitprm1  13685  hashfun  14351  hashf1  14371  hashtpg  14399  cshword  14705  wrd2pr2op  14857  wrd3tpop  14862  relexpsucrd  14947  relexpsucld  14948  fsum2dlem  15684  fprod2dlem  15894  ef4p  16029  sin01bnd  16101  odd2np1  16259  bitsinvp1  16367  smumullem  16410  oppcmon  17653  issubc2  17751  curf1cl  18142  curfcl  18146  cnvtsr  18502  ex-chn1  18551  sylow1lem1  19518  sylow2a  19539  ablsimpgfindlem1  20029  coe1fzgsumdlem  22238  evl1gsumdlem  22291  pmatcollpw3lem  22718  pptbas  22943  2ndcctbss  23390  txcmplem1  23576  qtopeu  23651  alexsubALTlem3  23984  ustuqtop5  24180  psmetdmdm  24240  xmetdmdm  24270  pcopt  24969  pcorevlem  24973  voliunlem1  25498  i1fima2  25627  iblabs  25777  dveflem  25930  deg1val  26048  abssinper  26477  mulcxplem  26640  dvatan  26892  lgamgulmlem2  26987  lgamgulmlem5  26990  lgseisenlem1  27333  dchrisumlem1  27447  pntlemr  27560  negsdi  28012  noseqrdg0  28257  eucliddivs  28321  pw2cut2  28402  krippenlem  28688  cusgredg  29423  cusgrsizeindb0  29449  numclwlk1lem1  30370  numclwwlk3lem2lem  30384  grporndm  30511  vafval  30604  smfval  30606  hvmul0  31025  cmcmlem  31592  cmbr3i  31601  nmbdfnlbi  32050  nmcfnlbi  32053  nmopcoadji  32102  pjin2i  32194  hst1h  32228  xaddeq0  32761  sgnmul  32844  gsumhashmul  33078  cycpmconjslem1  33164  archirngz  33199  opprqusmulr  33500  esplyind  33659  extdgfialglem2  33778  constrinvcl  33858  cos9thpiminplylem1  33867  esumcst  34148  eulerpartlems  34445  dstfrvunirn  34560  subfacp1lem5  35300  cvmliftlem10  35410  fnessref  36473  fnemeet2  36483  poimirlem4  37737  poimirlem19  37752  poimirlem20  37753  poimirlem23  37756  poimirlem24  37757  poimirlem25  37758  poimirlem28  37761  ovoliunnfl  37775  voliunnfl  37777  volsupnfl  37778  itg2addnclem  37784  itg2addnc  37787  iblabsnc  37797  iblmulc2nc  37798  sdclem2  37855  blbnd  37900  ismgmOLD  37963  ismndo2  37987  rnresequniqs  38439  tendo0co2  40960  dvhfvadd  41263  dvh4dimN  41619  mzpcompact2lem  42908  diophrw  42916  eldioph2  42919  pellexlem5  42990  pell1qr1  43028  rmxy0  43080  wessf1ornlem  45345  cncfuni  46046  cncfiooicclem1  46053  dvnprodlem1  46106  fourierdlem38  46305  fourierdlem60  46326  fourierdlem61  46327  fourierdlem79  46345  fourierdlem112  46378  fourierswlem  46390  fouriersw  46391  chnerlem1  47042  fvmptrab  47454  fvmptrabdm  47455  fmtnofac2  47731  nn0sumshdiglem1  48783  eloprab1st2nd  49029  dmdm  49214  isinito2lem  49659  termolmd  49831