Theorem eqtr2di 2793

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 2792	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2742	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 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  eqtr4id  2795  csbin  4379  csbif  4522  csbuni  4876  csbima12  5997  somincom  6054  resresdm  6151  iotauni2  6427  csbfv12  6849  opabiotafun  6881  fvmptrabfv  6938  fndifnfp  7080  elxp4  7801  elxp5  7802  fo1stres  7889  fo2ndres  7890  eloprabi  7935  fo2ndf  7993  seqomlem2  8313  oev2  8384  odi  8441  fundmen  8856  xpsnen  8880  xpassen  8891  ac6sfi  9102  infeq5  9439  alephsuc3  10382  rankcf  10579  ine0  11456  nn0n0n1ge2  12346  fzval2  13288  fseq1p1m1  13376  fzosplitprm1  13543  hashfun  14197  hashf1  14216  hashtpg  14244  cshword  14549  wrd2pr2op  14701  wrd3tpop  14706  relexpsucrd  14789  relexpsucld  14790  fsum2dlem  15527  fprod2dlem  15735  ef4p  15867  sin01bnd  15939  odd2np1  16095  bitsinvp1  16201  smumullem  16244  oppcmon  17495  issubc2  17596  curf1cl  17991  curfcl  17995  cnvtsr  18351  sylow1lem1  19248  sylow2a  19269  ablsimpgfindlem1  19755  coe1fzgsumdlem  21517  evl1gsumdlem  21567  pmatcollpw3lem  21977  pptbas  22203  2ndcctbss  22651  txcmplem1  22837  qtopeu  22912  alexsubALTlem3  23245  ustuqtop5  23442  psmetdmdm  23503  xmetdmdm  23533  pcopt  24230  pcorevlem  24234  voliunlem1  24759  i1fima2  24888  iblabs  25038  dveflem  25188  deg1val  25306  abssinper  25722  mulcxplem  25884  dvatan  26130  lgamgulmlem2  26224  lgamgulmlem5  26227  lgseisenlem1  26568  dchrisumlem1  26682  pntlemr  26795  krippenlem  27096  cusgredg  27836  cusgrsizeindb0  27861  numclwlk1lem1  28778  numclwwlk3lem2lem  28792  grporndm  28917  vafval  29010  smfval  29012  hvmul0  29431  cmcmlem  29998  cmbr3i  30007  nmbdfnlbi  30456  nmcfnlbi  30459  nmopcoadji  30508  pjin2i  30600  hst1h  30634  xaddeq0  31121  gsumhashmul  31361  cycpmconjslem1  31466  archirngz  31488  esumcst  32076  eulerpartlems  32372  dstfrvunirn  32486  sgnmul  32554  subfacp1lem5  33191  cvmliftlem10  33301  fnessref  34591  fnemeet2  34601  poimirlem4  35825  poimirlem19  35840  poimirlem20  35841  poimirlem23  35844  poimirlem24  35845  poimirlem25  35846  poimirlem28  35849  ovoliunnfl  35863  voliunnfl  35865  volsupnfl  35866  itg2addnclem  35872  itg2addnc  35875  iblabsnc  35885  iblmulc2nc  35886  sdclem2  35944  blbnd  35989  ismgmOLD  36052  ismndo2  36076  rnresequniqs  36509  tendo0co2  38844  dvhfvadd  39147  dvh4dimN  39503  mzpcompact2lem  40610  diophrw  40618  eldioph2  40621  pellexlem5  40692  pell1qr1  40730  rmxy0  40783  wessf1ornlem  42766  cncfuni  43476  cncfiooicclem1  43483  fourierdlem38  43735  fourierdlem60  43756  fourierdlem61  43757  fourierdlem79  43775  fourierdlem112  43808  fourierswlem  43820  fouriersw  43821  fvmptrab  44842  fvmptrabdm  44843  fmtnofac2  45079  nn0sumshdiglem1  46025