Theorem eqtr2di 2821

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqtr4id  2823  csbin  4405  csbif  4547  elpr2elpr  4835  csbuni  4904  csbima12  6079  somincom  6132  resresdm  6232  iotauni2  6506  csbfv12  6924  opabiotafun  6959  fvmptrabfv  7020  fndifnfp  7172  elxp4  7915  elxp5  7916  fo1stres  8008  fo2ndres  8009  sbcoteq1a  8044  eloprabi  8056  fo2ndf  8112  seqomlem2  8434  oev2  8504  odi  8560  fundmen  9024  xpsnen  9045  xpassen  9055  ac6sfi  9240  infeq5  9602  alephsuc3  10561  rankcf  10758  ine0  11645  nn0n0n1ge2  12568  fzval2  13534  fseq1p1m1  13622  fzosplitprm1  13803  hashfun  14470  hashf1  14490  hashtpg  14518  cshword  14824  wrd2pr2op  14976  wrd3tpop  14981  relexpsucrd  15066  relexpsucld  15067  sgnmul  15140  fsum2dlem  15817  fprod2dlem  16030  ef4p  16165  sin01bnd  16237  odd2np1  16395  bitsinvp1  16503  smumullem  16546  oppcmon  17791  issubc2  17889  curf1cl  18280  curfcl  18284  cnvtsr  18640  ex-chn1  18689  sylow1lem1  19664  sylow2a  19685  ablsimpgfindlem1  20175  coe1fzgsumdlem  22428  evl1gsumdlem  22481  pmatcollpw3lem  22905  pptbas  23130  2ndcctbss  23577  txcmplem1  23763  qtopeu  23838  alexsubALTlem3  24171  ustuqtop5  24367  psmetdmdm  24427  xmetdmdm  24457  pcopt  25146  pcorevlem  25150  voliunlem1  25674  i1fima2  25803  iblabs  25953  dveflem  26103  deg1val  26218  abssinper  26648  mulcxplem  26811  dvatan  27062  lgamgulmlem2  27156  lgamgulmlem5  27159  lgseisenlem1  27501  dchrisumlem1  27615  pntlemr  27728  negsdi  28205  noseqrdg0  28462  eucliddivs  28531  pw2cut2  28617  krippenlem  28925  cusgredg  29711  cusgrsizeindb0  29736  numclwlk1lem1  30657  numclwwlk3lem2lem  30671  grporndm  30799  vafval  30892  smfval  30894  hvmul0  31313  cmcmlem  31880  cmbr3i  31889  nmbdfnlbi  32338  nmcfnlbi  32341  nmopcoadji  32390  pjin2i  32482  hst1h  32516  xaddeq0  33035  gsumhashmul  33324  cycpmconjslem1  33411  archirngz  33446  opprqusmulr  33714  dflringlem3  33727  dflring4  33729  selvply1rhm0  33857  esplyfvaln  33905  esplyind  33906  extdgfialglem2  34024  constrinvcl  34104  cos9thpiminplylem1  34113  esumcst  34394  eulerpartlems  34691  dstfrvunirn  34806  subfacp1lem5  35571  cvmliftlem10  35681  fnessref  36753  fnemeet2  36763  poimirlem4  38158  poimirlem19  38173  poimirlem20  38174  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem28  38182  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  itg2addnclem  38205  itg2addnc  38208  iblabsnc  38218  iblmulc2nc  38219  sdclem2  38276  blbnd  38321  ismgmOLD  38384  ismndo2  38408  rnresequniqs  38868  tendo0co2  41447  dvhfvadd  41750  dvh4dimN  42106  mzpcompact2lem  43369  diophrw  43377  eldioph2  43380  pellexlem5  43447  pell1qr1  43485  rmxy0  43537  wessf1ornlem  45790  cncfuni  46487  cncfiooicclem1  46494  dvnprodlem1  46547  fourierdlem38  46746  fourierdlem60  46767  fourierdlem61  46768  fourierdlem79  46786  fourierdlem112  46819  fourierswlem  46831  fouriersw  46832  chnerlem1  47485  fvmptrab  47913  fvmptrabdm  47914  fmtnofac2  48205  nn0sumshdiglem1  49281  eloprab1st2nd  49526  dmdm  49711  isinito2lem  50156  termolmd  50328