Theorem eqtr3di 2786

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  resdmdfsn  5996  f0dom0  6724  f1o00  6815  fmpt  7062  fmptsn  7122  fninfp  7129  uniordint  7755  fsuppeq  8125  fsuppeqg  8126  mapsnd  8834  sbthlem4  9028  sbthlem6  9030  findcard2s  9100  ssfi  9107  elfiun  9343  cnfcom2  9623  rankxplim3  9805  rankxpsuc  9806  pm54.43  9925  axdc3lem4  10375  gruun  10729  recmulnq  10887  reclem3pr  10972  xrmineq  13132  xadddi2  13249  iooval2  13331  hashsng  14331  hashfun  14399  hashbc  14415  swrds2m  14903  isumclim3  15721  isummulc2  15724  iprodclim3  15965  bpolydiflem  16019  bpoly4  16024  fprodefsum  16060  ruclem4  16201  bitsshft  16444  phimullem  16749  pythagtriplem1  16787  1arithlem4  16897  fsets  17139  topnid  17398  submefmnd  18863  pgrpsubgsymg  19384  odhash  19549  gsumzf1o  19887  gsumdifsnd  19936  pgpfaclem1  20058  fincygsubgodd  20089  subdrgint  20780  mplcoe1  22015  mplcoe5  22018  evlslem4  22054  ordtrest2  23169  ufildr  23896  tsmsres  24109  zlmclm  25079  cphipval2  25208  csschl  25343  rrxcph  25359  volinun  25513  uniioombllem4  25553  itg1climres  25681  limcco  25860  vieta1lem2  26277  coseq00topi  26466  tangtx  26469  coskpi  26487  advlog  26618  advlogexp  26619  logtayl  26624  logccv  26627  dvcxp1  26704  dvcncxp1  26707  loglesqrt  26725  ang180lem3  26775  dquart  26817  atans2  26895  basellem8  27051  chtub  27175  bposlem6  27252  lgsquadlem2  27344  logdivsum  27496  log2sumbnd  27507  nodenselem5  27652  oldsuc  27878  precsexlem3  28201  spthispth  29792  ipval3  30780  siii  30924  cm2j  31691  pjssmii  31752  opsqrlem1  32211  hmopidmchi  32222  hmopidmpji  32223  pjcmul1i  32272  mddmd2  32380  cvexchlem  32439  dmdbr6ati  32494  difeq  32588  difuncomp  32623  ffsrn  32801  fzo0opth  32876  symgcom2  33145  cycpmcl  33177  cycpm2tr  33180  rhmimaidl  33492  drngidlhash  33494  1arithidomlem2  33596  qusdimsum  33772  2sqr3minply  33924  cos9thpiminplylem2  33927  zarcmplem  34025  ordtprsuni  34063  ordtrest2NEW  34067  zzsnm  34103  measun  34355  sxbrsigalem2  34430  carsgsigalem  34459  eulerpartlemgu  34521  gsumnunsn  34685  signsplypnf  34694  logdivsqrle  34794  cvmlift2lem12  35496  satf0suc  35558  nepss  35900  fwddifnp1  36347  finxpreclem1  37705  finxpreclem3  37709  poimirlem31  37972  ismblfin  37982  dvtan  37991  itg2addnclem3  37994  dvasin  38025  dvacos  38026  dvreasin  38027  dvreacos  38028  areacirclem1  38029  cnvepima  38658  disjimeceqim  39125  glbconN  39823  pmodl42N  40297  2polssN  40361  cdleme20j  40764  trlcocnv  41166  trlcone  41174  lclkrlem2c  41955  readvrec2  42793  sn-00idlem3  42832  sn-mul01  42858  selvvvval  43018  diophrw  43191  wopprc  43458  onuniintrab  43654  fsovcnvlem  44440  sineq0ALT  45363  founiiun0  45620  iccdifioo  45945  itgvol0  46396  fourierdlem33  46568  etransclem32  46694  simpcntrab  47298  chnsubseqwl  47309  sin5tlem1  47321  cycl3grtrilem  48422  gpg3kgrtriexlem2  48560  gpgprismgr4cycllem3  48573  gsumdifsndf  48657  zlmodzxzadd  48834  cosn  49309  oppcendc  49493  resccatlem  49548  resccat  49549  0funcg2  49559  imaf1hom  49583