Theorem eqtr2di 2791

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqtr4id  2793  csbin  4370  csbif  4512  elpr2elpr  4800  csbuni  4868  csbima12  6031  somincom  6084  resresdm  6184  iotauni2  6457  csbfv12  6872  opabiotafun  6907  fvmptrabfv  6968  fndifnfp  7120  elxp4  7862  elxp5  7863  fo1stres  7957  fo2ndres  7958  sbcoteq1a  7993  eloprabi  8005  fo2ndf  8060  seqomlem2  8380  oev2  8448  odi  8504  fundmen  8968  xpsnen  8989  xpassen  8999  ac6sfi  9184  infeq5  9549  alephsuc3  10494  rankcf  10691  ine0  11576  nn0n0n1ge2  12496  fzval2  13455  fseq1p1m1  13543  fzosplitprm1  13724  hashfun  14390  hashf1  14410  hashtpg  14438  cshword  14744  wrd2pr2op  14896  wrd3tpop  14901  relexpsucrd  14986  relexpsucld  14987  fsum2dlem  15723  fprod2dlem  15936  ef4p  16071  sin01bnd  16143  odd2np1  16301  bitsinvp1  16409  smumullem  16452  oppcmon  17696  issubc2  17794  curf1cl  18185  curfcl  18189  cnvtsr  18545  ex-chn1  18594  sylow1lem1  19564  sylow2a  19585  ablsimpgfindlem1  20075  coe1fzgsumdlem  22289  evl1gsumdlem  22342  pmatcollpw3lem  22766  pptbas  22991  2ndcctbss  23438  txcmplem1  23624  qtopeu  23699  alexsubALTlem3  24032  ustuqtop5  24228  psmetdmdm  24288  xmetdmdm  24318  pcopt  25007  pcorevlem  25011  voliunlem1  25535  i1fima2  25664  iblabs  25814  dveflem  25964  deg1val  26079  abssinper  26503  mulcxplem  26666  dvatan  26917  lgamgulmlem2  27011  lgamgulmlem5  27014  lgseisenlem1  27356  dchrisumlem1  27470  pntlemr  27583  negsdi  28060  noseqrdg0  28317  eucliddivs  28386  pw2cut2  28472  krippenlem  28776  cusgredg  29511  cusgrsizeindb0  29536  numclwlk1lem1  30457  numclwwlk3lem2lem  30471  grporndm  30599  vafval  30692  smfval  30694  hvmul0  31113  cmcmlem  31680  cmbr3i  31689  nmbdfnlbi  32138  nmcfnlbi  32141  nmopcoadji  32190  pjin2i  32282  hst1h  32316  xaddeq0  32845  sgnmul  32927  gsumhashmul  33148  cycpmconjslem1  33235  archirngz  33270  opprqusmulr  33574  selvply1rhm0  33710  esplyfvaln  33758  esplyind  33759  extdgfialglem2  33877  constrinvcl  33957  cos9thpiminplylem1  33966  esumcst  34247  eulerpartlems  34544  dstfrvunirn  34659  subfacp1lem5  35412  cvmliftlem10  35522  fnessref  36585  fnemeet2  36595  poimirlem4  37991  poimirlem19  38006  poimirlem20  38007  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem28  38015  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  itg2addnclem  38038  itg2addnc  38041  iblabsnc  38051  iblmulc2nc  38052  sdclem2  38109  blbnd  38154  ismgmOLD  38217  ismndo2  38241  rnresequniqs  38701  tendo0co2  41280  dvhfvadd  41583  dvh4dimN  41939  mzpcompact2lem  43200  diophrw  43208  eldioph2  43211  pellexlem5  43278  pell1qr1  43316  rmxy0  43368  wessf1ornlem  45632  cncfuni  46329  cncfiooicclem1  46336  dvnprodlem1  46389  fourierdlem38  46588  fourierdlem60  46609  fourierdlem61  46610  fourierdlem79  46628  fourierdlem112  46661  fourierswlem  46673  fouriersw  46674  chnerlem1  47327  fvmptrab  47755  fvmptrabdm  47756  fmtnofac2  48047  nn0sumshdiglem1  49112  eloprab1st2nd  49358  dmdm  49543  isinito2lem  49988  termolmd  50160