Theorem eqtr3di 2785

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 2739	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2783	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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  resdmdfsn  6030  f0dom0  6774  f1o00  6867  fmpt  7110  fmptsn  7166  fninfp  7173  uniordint  7791  fsuppeq  8162  fsuppeqg  8163  mapsnd  8882  sbthlem4  9088  sbthlem6  9090  findcard2s  9167  ssfi  9175  elfiun  9427  cnfcom2  9699  rankxplim3  9878  rankxpsuc  9879  pm54.43  9998  axdc3lem4  10450  gruun  10803  recmulnq  10961  reclem3pr  11046  xrmineq  13163  xadddi2  13280  iooval2  13361  hashsng  14333  hashfun  14401  hashbc  14416  swrds2m  14896  isumclim3  15709  isummulc2  15712  iprodclim3  15948  bpolydiflem  16002  bpoly4  16007  fprodefsum  16042  ruclem4  16181  bitsshft  16420  phimullem  16716  pythagtriplem1  16753  1arithlem4  16863  fsets  17106  topnid  17385  submefmnd  18812  pgrpsubgsymg  19318  odhash  19483  gsumzf1o  19821  gsumdifsnd  19870  pgpfaclem1  19992  fincygsubgodd  20023  subdrgint  20562  mplcoe1  21811  mplcoe5  21814  evlslem4  21856  ordtrest2  22928  ufildr  23655  tsmsres  23868  zlmclm  24859  cphipval2  24989  csschl  25124  rrxcph  25140  volinun  25295  uniioombllem4  25335  itg1climres  25464  limcco  25642  vieta1lem2  26060  coseq00topi  26248  tangtx  26251  coskpi  26268  advlog  26398  advlogexp  26399  logtayl  26404  logccv  26407  dvcxp1  26484  dvcncxp1  26487  loglesqrt  26502  ang180lem3  26552  dquart  26594  atans2  26672  basellem8  26828  chtub  26951  bposlem6  27028  lgsquadlem2  27120  logdivsum  27272  log2sumbnd  27283  nodenselem5  27427  oldsuc  27617  precsexlem3  27894  spthispth  29250  ipval3  30229  siii  30373  cm2j  31140  pjssmii  31201  opsqrlem1  31660  hmopidmchi  31671  hmopidmpji  31672  pjcmul1i  31721  mddmd2  31829  cvexchlem  31888  dmdbr6ati  31943  difeq  32023  difuncomp  32052  ffsrn  32221  symgcom2  32515  cycpmcl  32545  cycpm2tr  32548  rhmimaidl  32824  drngidlhash  32826  qusdimsum  33001  zarcmplem  33159  ordtprsuni  33197  ordtrest2NEW  33201  zzsnm  33237  measun  33507  sxbrsigalem2  33583  carsgsigalem  33612  eulerpartlemgu  33674  gsumnunsn  33850  signsplypnf  33859  logdivsqrle  33960  cvmlift2lem12  34603  satf0suc  34665  nepss  34991  fwddifnp1  35441  finxpreclem1  36573  finxpreclem3  36577  poimirlem31  36822  ismblfin  36832  dvtan  36841  itg2addnclem3  36844  dvasin  36875  dvacos  36876  dvreasin  36877  dvreacos  36878  areacirclem1  36879  cnvepima  37509  glbconN  38550  glbconNOLD  38551  pmodl42N  39025  2polssN  39089  cdleme20j  39492  trlcocnv  39894  trlcone  39902  lclkrlem2c  40683  selvvvval  41459  sn-mul01  41600  diophrw  41799  wopprc  42071  onuniintrab  42277  fsovcnvlem  43066  sineq0ALT  44000  founiiun0  44187  iccdifioo  44526  itgvol0  44982  fourierdlem33  45154  etransclem32  45280  simpcntrab  45884  gsumdifsndf  46857  zlmodzxzadd  47122