Theorem eqtr2di 2795

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

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  eqtr4id  2797  csbin  4354  csbif  4496  csbuni  4850  csbima12  5947  somincom  5999  resresdm  6096  csbfv12  6760  opabiotafun  6792  fvmptrabfv  6849  fndifnfp  6991  elxp4  7700  elxp5  7701  fo1stres  7787  fo2ndres  7788  eloprabi  7833  fo2ndf  7890  seqomlem2  8187  oev2  8250  odi  8307  fundmen  8708  xpsnen  8729  xpassen  8739  ac6sfi  8915  infeq5  9252  alephsuc3  10194  rankcf  10391  ine0  11267  nn0n0n1ge2  12157  fzval2  13098  fseq1p1m1  13186  fzosplitprm1  13352  hashfun  14004  hashf1  14023  hashtpg  14051  cshword  14356  wrd2pr2op  14508  wrd3tpop  14513  relexpsucrd  14596  relexpsucld  14597  fsum2dlem  15334  fprod2dlem  15542  ef4p  15674  sin01bnd  15746  odd2np1  15902  bitsinvp1  16008  smumullem  16051  oppcmon  17243  issubc2  17342  curf1cl  17736  curfcl  17740  cnvtsr  18094  sylow1lem1  18987  sylow2a  19008  ablsimpgfindlem1  19494  coe1fzgsumdlem  21222  evl1gsumdlem  21272  pmatcollpw3lem  21680  pptbas  21905  2ndcctbss  22352  txcmplem1  22538  qtopeu  22613  alexsubALTlem3  22946  ustuqtop5  23143  psmetdmdm  23203  xmetdmdm  23233  pcopt  23919  pcorevlem  23923  voliunlem1  24447  i1fima2  24576  iblabs  24726  dveflem  24876  deg1val  24994  abssinper  25410  mulcxplem  25572  dvatan  25818  lgamgulmlem2  25912  lgamgulmlem5  25915  lgseisenlem1  26256  dchrisumlem1  26370  pntlemr  26483  krippenlem  26781  cusgredg  27512  cusgrsizeindb0  27537  numclwlk1lem1  28452  numclwwlk3lem2lem  28466  grporndm  28591  vafval  28684  smfval  28686  hvmul0  29105  cmcmlem  29672  cmbr3i  29681  nmbdfnlbi  30130  nmcfnlbi  30133  nmopcoadji  30182  pjin2i  30274  hst1h  30308  xaddeq0  30796  gsumhashmul  31035  cycpmconjslem1  31140  archirngz  31162  esumcst  31743  eulerpartlems  32039  dstfrvunirn  32153  sgnmul  32221  subfacp1lem5  32859  cvmliftlem10  32969  fnessref  34283  fnemeet2  34293  poimirlem4  35518  poimirlem19  35533  poimirlem20  35534  poimirlem23  35537  poimirlem24  35538  poimirlem25  35539  poimirlem28  35542  ovoliunnfl  35556  voliunnfl  35558  volsupnfl  35559  itg2addnclem  35565  itg2addnc  35568  iblabsnc  35578  iblmulc2nc  35579  sdclem2  35637  blbnd  35682  ismgmOLD  35745  ismndo2  35769  rnresequniqs  36204  tendo0co2  38539  dvhfvadd  38842  dvh4dimN  39198  mzpcompact2lem  40276  diophrw  40284  eldioph2  40287  pellexlem5  40358  pell1qr1  40396  rmxy0  40448  wessf1ornlem  42395  cncfuni  43102  cncfiooicclem1  43109  fourierdlem38  43361  fourierdlem60  43382  fourierdlem61  43383  fourierdlem79  43401  fourierdlem112  43434  fourierswlem  43446  fouriersw  43447  fvmptrab  44456  fvmptrabdm  44457  fmtnofac2  44694  nn0sumshdiglem1  45640