Theorem eqtr2di 2794

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 2793	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2743	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqtr4id  2796  csbin  4442  csbif  4583  elpr2elpr  4869  csbuni  4936  csbima12  6097  somincom  6154  resresdm  6253  iotauni2  6530  csbfv12  6954  opabiotafun  6989  fvmptrabfv  7048  fndifnfp  7196  elxp4  7944  elxp5  7945  fo1stres  8040  fo2ndres  8041  sbcoteq1a  8076  eloprabi  8088  fo2ndf  8146  seqomlem2  8491  oev2  8561  odi  8617  fundmen  9071  xpsnen  9095  xpassen  9106  ac6sfi  9320  infeq5  9677  alephsuc3  10620  rankcf  10817  ine0  11698  nn0n0n1ge2  12594  fzval2  13550  fseq1p1m1  13638  fzosplitprm1  13816  hashfun  14476  hashf1  14496  hashtpg  14524  cshword  14829  wrd2pr2op  14982  wrd3tpop  14987  relexpsucrd  15072  relexpsucld  15073  fsum2dlem  15806  fprod2dlem  16016  ef4p  16149  sin01bnd  16221  odd2np1  16378  bitsinvp1  16486  smumullem  16529  oppcmon  17782  issubc2  17881  curf1cl  18273  curfcl  18277  cnvtsr  18633  sylow1lem1  19616  sylow2a  19637  ablsimpgfindlem1  20127  coe1fzgsumdlem  22307  evl1gsumdlem  22360  pmatcollpw3lem  22789  pptbas  23015  2ndcctbss  23463  txcmplem1  23649  qtopeu  23724  alexsubALTlem3  24057  ustuqtop5  24254  psmetdmdm  24315  xmetdmdm  24345  pcopt  25055  pcorevlem  25059  voliunlem1  25585  i1fima2  25714  iblabs  25864  dveflem  26017  deg1val  26135  abssinper  26563  mulcxplem  26726  dvatan  26978  lgamgulmlem2  27073  lgamgulmlem5  27076  lgseisenlem1  27419  dchrisumlem1  27533  pntlemr  27646  negsdi  28082  noseqrdg0  28313  krippenlem  28698  cusgredg  29441  cusgrsizeindb0  29467  numclwlk1lem1  30388  numclwwlk3lem2lem  30402  grporndm  30529  vafval  30622  smfval  30624  hvmul0  31043  cmcmlem  31610  cmbr3i  31619  nmbdfnlbi  32068  nmcfnlbi  32071  nmopcoadji  32120  pjin2i  32212  hst1h  32246  xaddeq0  32757  gsumhashmul  33064  cycpmconjslem1  33174  archirngz  33196  opprqusmulr  33519  esumcst  34064  eulerpartlems  34362  dstfrvunirn  34477  sgnmul  34545  subfacp1lem5  35189  cvmliftlem10  35299  fnessref  36358  fnemeet2  36368  poimirlem4  37631  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnclem  37678  itg2addnc  37681  iblabsnc  37691  iblmulc2nc  37692  sdclem2  37749  blbnd  37794  ismgmOLD  37857  ismndo2  37881  rnresequniqs  38333  tendo0co2  40790  dvhfvadd  41093  dvh4dimN  41449  mzpcompact2lem  42762  diophrw  42770  eldioph2  42773  pellexlem5  42844  pell1qr1  42882  rmxy0  42935  wessf1ornlem  45190  cncfuni  45901  cncfiooicclem1  45908  dvnprodlem1  45961  fourierdlem38  46160  fourierdlem60  46181  fourierdlem61  46182  fourierdlem79  46200  fourierdlem112  46233  fourierswlem  46245  fouriersw  46246  fvmptrab  47304  fvmptrabdm  47305  fmtnofac2  47556  nn0sumshdiglem1  48542