Theorem eqtr2di 2817

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  eqtr4id  2819  csbin  4407  csbif  4547  elpr2elpr  4836  csbuni  4905  csbima12  6083  somincom  6136  resresdm  6236  iotauni2  6512  csbfv12  6930  opabiotafun  6965  fvmptrabfv  7026  fndifnfp  7178  elxp4  7921  elxp5  7922  fo1stres  8014  fo2ndres  8015  sbcoteq1a  8050  eloprabi  8062  fo2ndf  8118  seqomlem2  8440  oev2  8510  odi  8566  fundmen  9031  xpsnen  9052  xpassen  9062  ac6sfi  9247  infeq5  9609  alephsuc3  10576  rankcf  10773  ine0  11660  nn0n0n1ge2  12583  fzval2  13550  fseq1p1m1  13639  fzosplitprm1  13820  hashfun  14488  hashf1  14508  hashtpg  14536  cshword  14848  wrd2pr2op  15000  wrd3tpop  15005  relexpsucrd  15090  relexpsucld  15091  sgnmul  15164  fsum2dlem  15840  fprod2dlem  16053  ef4p  16187  sin01bnd  16259  odd2np1  16417  bitsinvp1  16525  smumullem  16568  oppcmon  17813  issubc2  17911  curf1cl  18302  curfcl  18306  cnvtsr  18662  ex-chn1  18711  sylow1lem1  19692  sylow2a  19713  ablsimpgfindlem1  20203  coe1fzgsumdlem  22493  evl1gsumdlem  22546  pmatcollpw3lem  22970  pptbas  23195  2ndcctbss  23643  txcmplem1  23829  qtopeu  23904  alexsubALTlem3  24237  ustuqtop5  24433  psmetdmdm  24493  xmetdmdm  24523  pcopt  25212  pcorevlem  25216  voliunlem1  25740  i1fima2  25869  iblabs  26019  dveflem  26169  deg1val  26284  abssinper  26717  mulcxplem  26880  dvatan  27131  lgamgulmlem2  27225  lgamgulmlem5  27228  lgseisenlem1  27570  dchrisumlem1  27684  pntlemr  27797  negsdi  28274  noseqrdg0  28531  eucliddivs  28600  pw2cut2  28686  krippenlem  28998  prlngmid2  29242  cusgredg  29808  cusgrsizeindb0  29833  numclwlk1lem1  30767  numclwwlk3lem2lem  30781  grporndm  30909  vafval  31002  smfval  31004  hvmul0  31423  cmcmlem  31990  cmbr3i  31999  nmbdfnlbi  32448  nmcfnlbi  32451  nmopcoadji  32500  pjin2i  32592  hst1h  32626  xaddeq0  33144  gsumhashmul  33427  cycpmconjslem1  33514  archirngz  33549  opprqusmulr  33813  dflringlem3  33826  dflring4  33828  selvply1rhm0  33956  esplyfvaln  34004  esplyind  34005  extdgfialglem2  34123  constrinvcl  34203  cos9thpiminplylem1  34212  esumcst  34493  eulerpartlems  34791  dstfrvunirn  34906  subfacp1lem5  35689  cvmliftlem10  35799  fnessref  36901  fnemeet2  36911  poimirlem4  38308  poimirlem19  38323  poimirlem20  38324  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem28  38332  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  itg2addnclem  38355  itg2addnc  38358  iblabsnc  38368  iblmulc2nc  38369  sdclem2  38426  blbnd  38471  ismgmOLD  38534  ismndo2  38558  rnresequniqs  39016  tendo0co2  41595  dvhfvadd  41898  dvh4dimN  42254  mzpcompact2lem  43515  diophrw  43523  eldioph2  43526  pellexlem5  43593  pell1qr1  43631  rmxy0  43683  wessf1ornlem  45936  cncfuni  46633  cncfiooicclem1  46640  dvnprodlem1  46693  fourierdlem38  46892  fourierdlem60  46913  fourierdlem61  46914  fourierdlem79  46932  fourierdlem112  46965  fourierswlem  46977  fouriersw  46978  chnerlem1  47631  fvmptrab  48062  fvmptrabdm  48063  fmtnofac2  48354  nn0sumshdiglem1  49434  eloprab1st2nd  49679  dmdm  49864  isinito2lem  50309  termolmd  50481