Theorem eqtr3di 2789

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  resdmdfsn  5983  f0dom0  6711  f1o00  6802  fmpt  7051  fmptsn  7111  fninfp  7118  uniordint  7744  fsuppeq  8115  fsuppeqg  8116  mapsnd  8824  sbthlem4  9018  sbthlem6  9020  findcard2s  9090  ssfi  9097  elfiun  9333  cnfcom2  9614  rankxplim3  9796  rankxpsuc  9797  pm54.43  9916  axdc3lem4  10366  gruun  10720  recmulnq  10878  reclem3pr  10963  xrmineq  13123  xadddi2  13240  iooval2  13322  hashsng  14322  hashfun  14390  hashbc  14406  swrds2m  14894  isumclim3  15712  isummulc2  15715  iprodclim3  15956  bpolydiflem  16010  bpoly4  16015  fprodefsum  16051  ruclem4  16192  bitsshft  16435  phimullem  16740  pythagtriplem1  16778  1arithlem4  16888  fsets  17130  topnid  17389  submefmnd  18854  pgrpsubgsymg  19375  odhash  19540  gsumzf1o  19878  gsumdifsnd  19927  pgpfaclem1  20049  fincygsubgodd  20080  subdrgint  20775  mplcoe1  22013  mplcoe5  22016  evlslem4  22052  selvvvval  22118  ordtrest2  23187  ufildr  23914  tsmsres  24127  zlmclm  25097  cphipval2  25226  csschl  25361  rrxcph  25377  volinun  25531  uniioombllem4  25571  itg1climres  25699  limcco  25878  vieta1lem2  26295  coseq00topi  26484  tangtx  26487  coskpi  26505  advlog  26636  advlogexp  26637  logtayl  26642  logccv  26645  dvcxp1  26722  dvcncxp1  26725  loglesqrt  26743  ang180lem3  26793  dquart  26835  atans2  26913  basellem8  27069  chtub  27193  bposlem6  27270  lgsquadlem2  27362  logdivsum  27514  log2sumbnd  27525  nodenselem5  27670  oldsuc  27896  precsexlem3  28219  spthispth  29810  ipval3  30798  siii  30942  cm2j  31709  pjssmii  31770  opsqrlem1  32229  hmopidmchi  32240  hmopidmpji  32241  pjcmul1i  32290  mddmd2  32398  cvexchlem  32457  dmdbr6ati  32512  difeq  32606  difuncomp  32642  ffsrn  32820  fzo0opth  32895  symgcom2  33165  cycpmcl  33197  cycpm2tr  33200  rhmimaidl  33515  drngidlhash  33517  1arithidomlem2  33619  qusdimsum  33812  2sqr3minply  33964  cos9thpiminplylem2  33967  zarcmplem  34065  ordtprsuni  34103  ordtrest2NEW  34107  zzsnm  34143  measun  34395  sxbrsigalem2  34470  carsgsigalem  34499  eulerpartlemgu  34561  gsumnunsn  34725  signsplypnf  34734  logdivsqrle  34834  cvmlift2lem12  35542  satf0suc  35604  nepss  35946  fwddifnp1  36393  finxpreclem1  37751  finxpreclem3  37755  poimirlem31  38018  ismblfin  38028  dvtan  38037  itg2addnclem3  38040  dvasin  38071  dvacos  38072  dvreasin  38073  dvreacos  38074  areacirclem1  38075  cnvepima  38704  disjimeceqim  39171  glbconN  39869  pmodl42N  40343  2polssN  40407  cdleme20j  40810  trlcocnv  41212  trlcone  41220  lclkrlem2c  42001  readvrec2  42838  sn-00idlem3  42877  sn-mul01  42903  diophrw  43208  wopprc  43475  onuniintrab  43671  fsovcnvlem  44457  sineq0ALT  45380  founiiun0  45637  iccdifioo  45960  itgvol0  46411  fourierdlem33  46583  etransclem32  46709  simpcntrab  47313  chnsubseqwl  47324  sin5tlem1  47336  cycl3grtrilem  48437  gpg3kgrtriexlem2  48575  gpgprismgr4cycllem3  48588  gsumdifsndf  48672  zlmodzxzadd  48849  cosn  49324  oppcendc  49508  resccatlem  49563  resccat  49564  0funcg2  49574  imaf1hom  49598