Theorem eqtr3di 2810

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr3di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr3di.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3di	⊢ (𝜑 → 𝐵 = 𝐶)

Proof of Theorem eqtr3di

Step	Hyp	Ref	Expression
1		eqtr3di.2	. . 3 ⊢ 𝐴 = 𝐶
2	1	eqcomi 2769	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2808	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 2155  ax-ext 2732

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

This theorem is used by:  resdmdfsnOLD  6026  f0dom0  6759  f1o00  6853  fmpt  7103  fmptsn  7165  fninfp  7172  uniordint  7800  fsuppeq  8173  fsuppeqg  8174  mapsnd  8893  sbthlem4  9088  sbthlem6  9090  findcard2s  9160  ssfi  9167  elfiun  9400  cnfcom2  9681  rankxplim3  9863  rankxpsuc  9864  pm54.43  10006  axdc3lem4  10455  gruun  10815  recmulnq  10973  reclem3pr  11058  xrmineq  13232  xadddi2  13349  iooval2  13431  hashsng  14433  hashfun  14502  hashbc  14518  swrds2m  15012  isumclim3  15845  isummulc2  15848  iprodclim3  16087  bpolydiflem  16140  bpoly4  16145  fprodefsum  16181  ruclem4  16322  bitsshft  16565  phimullem  16870  pythagtriplem1  16908  1arithlem4  17018  fsets  17261  topnid  17520  submefmnd  19004  pgrpsubgsymg  19536  odhash  19701  gsumzf1o  20039  gsumdifsnd  20088  pgpfaclem1  20210  fincygsubgodd  20241  subdrgint  20969  mplcoe1  22253  mplcoe5  22256  evlslem4  22292  selvvvval  22358  ordtrest2  23429  ufildr  24157  tsmsres  24370  zlmclm  25340  cphipval2  25469  csschl  25604  rrxcph  25620  volinun  25774  uniioombllem4  25814  itg1climres  25942  limcco  26120  rnplynfin  26539  vieta1lem2  26543  coseq00topi  26740  tangtx  26743  coskpi  26760  advlog  26891  advlogexp  26892  logtayl  26897  logccv  26900  dvcxp1  26977  dvcncxp1  26980  loglesqrt  26998  ang180lem3  27048  dquart  27090  atans2  27168  basellem8  27324  chtub  27448  bposlem6  27525  lgsquadlem2  27617  logdivsum  27769  log2sumbnd  27780  nodenselem5  27924  oldsuc  28151  precsexlem3  28474  spthispth  30188  ipval3  31190  siii  31334  cm2j  32101  pjssmii  32162  opsqrlem1  32621  hmopidmchi  32632  hmopidmpji  32633  pjcmul1i  32682  mddmd2  32790  cvexchlem  32849  dmdbr6ati  32904  difeq  32993  difuncomp  33027  ffsrn  33199  fzo0opth  33274  symgcom2  33524  cycpmcl  33556  cycpm2tr  33559  rhmimaidl  33860  drngidlhash  33861  1arithidomlem2  33946  qusdimsum  34138  2sqr3minply  34290  cos9thpiminplylem2  34293  zarcmplem  34391  ordtprsuni  34429  ordtrest2NEW  34433  zzsnm  34469  measun  34722  sxbrsigalem2  34797  carsgsigalem  34826  eulerpartlemgu  34888  gsumnunsn  35052  signsplypnf  35058  logdivsqrle  35158  cvmlift2lem12  35893  satf0suc  35955  nepss  36297  fwddifnp1  36745  finxpreclem1  38143  finxpreclem3  38147  poimirlem3  38372  poimirlem31  38400  ismblfin  38410  dvtan  38419  itg2addnclem3  38422  dvasin  38453  dvacos  38454  dvreasin  38455  dvreacos  38456  areacirclem1  38457  cnvepima  39085  disjimeceqim  39552  glbconN  40250  pmodl42N  40724  2polssN  40788  cdleme20j  41191  trlcocnv  41593  trlcone  41601  lclkrlem2c  42382  readvrec2  43236  sn-00idlem3  43275  sn-mul01  43301  diophrw  43604  wopprc  43871  onuniintrab  44067  fsovcnvlem  44853  sineq0ALT  45759  founiiun0  46022  iccdifioo  46345  itgvol0  46796  fourierdlem33  46968  etransclem32  47094  simpcntrab  47698  chnsubseqwl  47707  sin5tlem1  47737  cycl3grtrilem  48862  gpg3kgrtriexlem2  49000  gpgprismgr4cycllem3  49013  gsumdifsndf  49096  zlmodzxzadd  49288  cosn  49762  oppcendc  49944  resccatlem  49999  resccat  50000  0funcg2  50010  imaf1hom  50034