Theorem eqtr2di 2792

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  eqtr4id  2794  csbin  4448  csbif  4588  elpr2elpr  4874  csbuni  4941  csbima12  6099  somincom  6157  resresdm  6255  iotauni2  6532  csbfv12  6955  opabiotafun  6989  fvmptrabfv  7048  fndifnfp  7196  elxp4  7945  elxp5  7946  fo1stres  8039  fo2ndres  8040  sbcoteq1a  8075  eloprabi  8087  fo2ndf  8145  seqomlem2  8490  oev2  8560  odi  8616  fundmen  9070  xpsnen  9094  xpassen  9105  ac6sfi  9318  infeq5  9675  alephsuc3  10618  rankcf  10815  ine0  11696  nn0n0n1ge2  12592  fzval2  13547  fseq1p1m1  13635  fzosplitprm1  13813  hashfun  14473  hashf1  14493  hashtpg  14521  cshword  14826  wrd2pr2op  14979  wrd3tpop  14984  relexpsucrd  15069  relexpsucld  15070  fsum2dlem  15803  fprod2dlem  16013  ef4p  16146  sin01bnd  16218  odd2np1  16375  bitsinvp1  16483  smumullem  16526  oppcmon  17786  issubc2  17887  curf1cl  18285  curfcl  18289  cnvtsr  18646  sylow1lem1  19631  sylow2a  19652  ablsimpgfindlem1  20142  coe1fzgsumdlem  22323  evl1gsumdlem  22376  pmatcollpw3lem  22805  pptbas  23031  2ndcctbss  23479  txcmplem1  23665  qtopeu  23740  alexsubALTlem3  24073  ustuqtop5  24270  psmetdmdm  24331  xmetdmdm  24361  pcopt  25069  pcorevlem  25073  voliunlem1  25599  i1fima2  25728  iblabs  25879  dveflem  26032  deg1val  26150  abssinper  26578  mulcxplem  26741  dvatan  26993  lgamgulmlem2  27088  lgamgulmlem5  27091  lgseisenlem1  27434  dchrisumlem1  27548  pntlemr  27661  negsdi  28097  noseqrdg0  28328  krippenlem  28713  cusgredg  29456  cusgrsizeindb0  29482  numclwlk1lem1  30398  numclwwlk3lem2lem  30412  grporndm  30539  vafval  30632  smfval  30634  hvmul0  31053  cmcmlem  31620  cmbr3i  31629  nmbdfnlbi  32078  nmcfnlbi  32081  nmopcoadji  32130  pjin2i  32222  hst1h  32256  xaddeq0  32764  gsumhashmul  33047  cycpmconjslem1  33157  archirngz  33179  opprqusmulr  33499  esumcst  34044  eulerpartlems  34342  dstfrvunirn  34456  sgnmul  34524  subfacp1lem5  35169  cvmliftlem10  35279  fnessref  36340  fnemeet2  36350  poimirlem4  37611  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem28  37635  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  itg2addnclem  37658  itg2addnc  37661  iblabsnc  37671  iblmulc2nc  37672  sdclem2  37729  blbnd  37774  ismgmOLD  37837  ismndo2  37861  rnresequniqs  38314  tendo0co2  40771  dvhfvadd  41074  dvh4dimN  41430  mzpcompact2lem  42739  diophrw  42747  eldioph2  42750  pellexlem5  42821  pell1qr1  42859  rmxy0  42912  wessf1ornlem  45128  cncfuni  45842  cncfiooicclem1  45849  dvnprodlem1  45902  fourierdlem38  46101  fourierdlem60  46122  fourierdlem61  46123  fourierdlem79  46141  fourierdlem112  46174  fourierswlem  46186  fouriersw  46187  fvmptrab  47242  fvmptrabdm  47243  fmtnofac2  47494  nn0sumshdiglem1  48471