Theorem eqtr3di 2812

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

Syntax hints:   → wi 4   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  resdmdfsnOLD  6019  f0dom0  6748  f1o00  6842  fmpt  7091  fmptsn  7151  fninfp  7158  uniordint  7784  fsuppeq  8155  fsuppeqg  8156  mapsnd  8868  sbthlem4  9062  sbthlem6  9064  findcard2s  9134  ssfi  9141  elfiun  9376  cnfcom2  9657  rankxplim3  9839  rankxpsuc  9840  pm54.43  9959  axdc3lem4  10410  gruun  10764  recmulnq  10922  reclem3pr  11007  xrmineq  13183  xadddi2  13300  iooval2  13382  hashsng  14382  hashfun  14450  hashbc  14466  swrds2m  14954  isumclim3  15786  isummulc2  15789  iprodclim3  16030  bpolydiflem  16084  bpoly4  16089  fprodefsum  16125  ruclem4  16266  bitsshft  16509  phimullem  16814  pythagtriplem1  16852  1arithlem4  16962  fsets  17205  topnid  17464  submefmnd  18929  pgrpsubgsymg  19449  odhash  19614  gsumzf1o  19952  gsumdifsnd  20001  pgpfaclem1  20123  fincygsubgodd  20154  subdrgint  20849  mplcoe1  22087  mplcoe5  22090  evlslem4  22126  selvvvval  22192  ordtrest2  23261  ufildr  23988  tsmsres  24201  zlmclm  25171  cphipval2  25300  csschl  25435  rrxcph  25451  volinun  25605  uniioombllem4  25645  itg1climres  25773  limcco  25952  vieta1lem2  26372  coseq00topi  26564  tangtx  26567  coskpi  26585  advlog  26716  advlogexp  26717  logtayl  26722  logccv  26725  dvcxp1  26802  dvcncxp1  26805  loglesqrt  26823  ang180lem3  26873  dquart  26915  atans2  26993  basellem8  27149  chtub  27273  bposlem6  27350  lgsquadlem2  27442  logdivsum  27594  log2sumbnd  27605  nodenselem5  27749  oldsuc  27976  precsexlem3  28299  spthispth  29921  ipval3  30909  siii  31053  cm2j  31820  pjssmii  31881  opsqrlem1  32340  hmopidmchi  32351  hmopidmpji  32352  pjcmul1i  32401  mddmd2  32509  cvexchlem  32568  dmdbr6ati  32623  difeq  32714  difuncomp  32750  ffsrn  32927  fzo0opth  33002  symgcom2  33261  cycpmcl  33293  cycpm2tr  33296  rhmimaidl  33615  drngidlhash  33617  1arithidomlem2  33729  qusdimsum  33922  2sqr3minply  34074  cos9thpiminplylem2  34077  zarcmplem  34175  ordtprsuni  34213  ordtrest2NEW  34217  zzsnm  34253  measun  34505  sxbrsigalem2  34580  carsgsigalem  34609  eulerpartlemgu  34671  gsumnunsn  34835  signsplypnf  34841  logdivsqrle  34941  cvmlift2lem12  35661  satf0suc  35723  nepss  36065  fwddifnp1  36512  finxpreclem1  37880  finxpreclem3  37884  poimirlem3  38119  poimirlem31  38147  ismblfin  38157  dvtan  38166  itg2addnclem3  38169  dvasin  38200  dvacos  38201  dvreasin  38202  dvreacos  38203  areacirclem1  38204  cnvepima  38833  disjimeceqim  39300  glbconN  39998  pmodl42N  40472  2polssN  40536  cdleme20j  40939  trlcocnv  41341  trlcone  41349  lclkrlem2c  42130  readvrec2  42967  sn-00idlem3  43006  sn-mul01  43032  diophrw  43337  wopprc  43604  onuniintrab  43800  fsovcnvlem  44586  sineq0ALT  45509  founiiun0  45765  iccdifioo  46088  itgvol0  46539  fourierdlem33  46711  etransclem32  46837  simpcntrab  47441  chnsubseqwl  47452  sin5tlem1  47464  cycl3grtrilem  48565  gpg3kgrtriexlem2  48703  gpgprismgr4cycllem3  48716  gsumdifsndf  48800  zlmodzxzadd  48977  cosn  49452  oppcendc  49636  resccatlem  49691  resccat  49692  0funcg2  49702  imaf1hom  49726