Theorem eqtr2di 2811

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751

This theorem is referenced by:  eqtr4id  2813  csbin  4329  csbif  4470  csbuni  4822  csbima12  5912  somincom  5959  resresdm  6055  csbfv12  6694  opabiotafun  6726  fvmptrabfv  6783  fndifnfp  6922  elxp4  7625  elxp5  7626  fo1stres  7712  fo2ndres  7713  eloprabi  7758  fo2ndf  7815  seqomlem2  8090  oev2  8151  odi  8208  fundmen  8595  xpsnen  8614  xpassen  8624  ac6sfi  8780  infeq5  9118  alephsuc3  10025  rankcf  10222  ine0  11098  nn0n0n1ge2  11986  fzval2  12927  fseq1p1m1  13015  fzosplitprm1  13181  hashfun  13833  hashf1  13852  hashtpg  13880  cshword  14185  wrd2pr2op  14337  wrd3tpop  14342  relexpsucrd  14425  relexpsucld  14426  fsum2dlem  15158  fprod2dlem  15367  ef4p  15499  sin01bnd  15571  odd2np1  15727  bitsinvp1  15833  smumullem  15876  oppcmon  17052  issubc2  17150  curf1cl  17529  curfcl  17533  cnvtsr  17883  sylow1lem1  18775  sylow2a  18796  ablsimpgfindlem1  19282  coe1fzgsumdlem  21010  evl1gsumdlem  21060  pmatcollpw3lem  21468  pptbas  21693  2ndcctbss  22140  txcmplem1  22326  qtopeu  22401  alexsubALTlem3  22734  ustuqtop5  22931  psmetdmdm  22992  xmetdmdm  23022  pcopt  23708  pcorevlem  23712  voliunlem1  24235  i1fima2  24364  iblabs  24513  dveflem  24663  deg1val  24781  abssinper  25197  mulcxplem  25359  dvatan  25605  lgamgulmlem2  25699  lgamgulmlem5  25702  lgseisenlem1  26043  dchrisumlem1  26157  pntlemr  26270  krippenlem  26568  cusgredg  27298  cusgrsizeindb0  27323  numclwlk1lem1  28238  numclwwlk3lem2lem  28252  grporndm  28377  vafval  28470  smfval  28472  hvmul0  28891  cmcmlem  29458  cmbr3i  29467  nmbdfnlbi  29916  nmcfnlbi  29919  nmopcoadji  29968  pjin2i  30060  hst1h  30094  xaddeq0  30585  gsumhashmul  30827  cycpmconjslem1  30932  archirngz  30954  esumcst  31535  eulerpartlems  31831  dstfrvunirn  31945  sgnmul  32013  subfacp1lem5  32647  cvmliftlem10  32757  fnessref  34080  fnemeet2  34090  poimirlem4  35326  poimirlem19  35341  poimirlem20  35342  poimirlem23  35345  poimirlem24  35346  poimirlem25  35347  poimirlem28  35350  ovoliunnfl  35364  voliunnfl  35366  volsupnfl  35367  itg2addnclem  35373  itg2addnc  35376  iblabsnc  35386  iblmulc2nc  35387  sdclem2  35445  blbnd  35490  ismgmOLD  35553  ismndo2  35577  rnresequniqs  36014  tendo0co2  38349  dvhfvadd  38652  dvh4dimN  39008  mzpcompact2lem  40050  diophrw  40058  eldioph2  40061  pellexlem5  40132  pell1qr1  40170  rmxy0  40222  wessf1ornlem  42166  cncfuni  42879  cncfiooicclem1  42886  fourierdlem38  43138  fourierdlem60  43159  fourierdlem61  43160  fourierdlem79  43178  fourierdlem112  43211  fourierswlem  43223  fouriersw  43224  fvmptrab  44201  fvmptrabdm  44202  fmtnofac2  44439  nn0sumshdiglem1  45385