Theorem eqtr3di 2795

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  resdmdfsn  6060  f0dom0  6805  f1o00  6897  fmpt  7144  fmptsn  7201  fninfp  7208  uniordint  7837  fsuppeq  8216  fsuppeqg  8217  mapsnd  8944  sbthlem4  9152  sbthlem6  9154  findcard2s  9231  ssfi  9240  elfiun  9499  cnfcom2  9771  rankxplim3  9950  rankxpsuc  9951  pm54.43  10070  axdc3lem4  10522  gruun  10875  recmulnq  11033  reclem3pr  11118  xrmineq  13242  xadddi2  13359  iooval2  13440  hashsng  14418  hashfun  14486  hashbc  14502  swrds2m  14990  isumclim3  15807  isummulc2  15810  iprodclim3  16048  bpolydiflem  16102  bpoly4  16107  fprodefsum  16143  ruclem4  16282  bitsshft  16521  phimullem  16826  pythagtriplem1  16863  1arithlem4  16973  fsets  17216  topnid  17495  submefmnd  18930  pgrpsubgsymg  19451  odhash  19616  gsumzf1o  19954  gsumdifsnd  20003  pgpfaclem1  20125  fincygsubgodd  20156  subdrgint  20826  mplcoe1  22078  mplcoe5  22081  evlslem4  22123  ordtrest2  23233  ufildr  23960  tsmsres  24173  zlmclm  25164  cphipval2  25294  csschl  25429  rrxcph  25445  volinun  25600  uniioombllem4  25640  itg1climres  25769  limcco  25948  vieta1lem2  26371  coseq00topi  26562  tangtx  26565  coskpi  26583  advlog  26714  advlogexp  26715  logtayl  26720  logccv  26723  dvcxp1  26800  dvcncxp1  26803  loglesqrt  26822  ang180lem3  26872  dquart  26914  atans2  26992  basellem8  27149  chtub  27274  bposlem6  27351  lgsquadlem2  27443  logdivsum  27595  log2sumbnd  27606  nodenselem5  27751  oldsuc  27942  precsexlem3  28251  zs12bday  28442  spthispth  29762  ipval3  30741  siii  30885  cm2j  31652  pjssmii  31713  opsqrlem1  32172  hmopidmchi  32183  hmopidmpji  32184  pjcmul1i  32233  mddmd2  32341  cvexchlem  32400  dmdbr6ati  32455  difeq  32548  difuncomp  32576  ffsrn  32743  fzo0opth  32810  symgcom2  33077  cycpmcl  33109  cycpm2tr  33112  rhmimaidl  33425  drngidlhash  33427  1arithidomlem2  33529  qusdimsum  33641  2sqr3minply  33738  zarcmplem  33827  ordtprsuni  33865  ordtrest2NEW  33869  zzsnm  33905  measun  34175  sxbrsigalem2  34251  carsgsigalem  34280  eulerpartlemgu  34342  gsumnunsn  34518  signsplypnf  34527  logdivsqrle  34627  cvmlift2lem12  35282  satf0suc  35344  nepss  35680  fwddifnp1  36129  finxpreclem1  37355  finxpreclem3  37359  poimirlem31  37611  ismblfin  37621  dvtan  37630  itg2addnclem3  37633  dvasin  37664  dvacos  37665  dvreasin  37666  dvreacos  37667  areacirclem1  37668  cnvepima  38293  glbconN  39333  glbconNOLD  39334  pmodl42N  39808  2polssN  39872  cdleme20j  40275  trlcocnv  40677  trlcone  40685  lclkrlem2c  41466  sn-mul01  42401  selvvvval  42540  diophrw  42715  wopprc  42987  onuniintrab  43187  fsovcnvlem  43975  sineq0ALT  44908  founiiun0  45097  iccdifioo  45433  itgvol0  45889  fourierdlem33  46061  etransclem32  46187  simpcntrab  46791  gsumdifsndf  47904  zlmodzxzadd  48083