Theorem eqtr3di 2781

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  resdmdfsn  5979  f0dom0  6707  f1o00  6798  fmpt  7043  fmptsn  7101  fninfp  7108  uniordint  7734  fsuppeq  8105  fsuppeqg  8106  mapsnd  8810  sbthlem4  9003  sbthlem6  9005  findcard2s  9075  ssfi  9082  elfiun  9314  cnfcom2  9592  rankxplim3  9774  rankxpsuc  9775  pm54.43  9894  axdc3lem4  10344  gruun  10697  recmulnq  10855  reclem3pr  10940  xrmineq  13079  xadddi2  13196  iooval2  13278  hashsng  14276  hashfun  14344  hashbc  14360  swrds2m  14848  isumclim3  15666  isummulc2  15669  iprodclim3  15907  bpolydiflem  15961  bpoly4  15966  fprodefsum  16002  ruclem4  16143  bitsshft  16386  phimullem  16690  pythagtriplem1  16728  1arithlem4  16838  fsets  17080  topnid  17339  submefmnd  18803  pgrpsubgsymg  19321  odhash  19486  gsumzf1o  19824  gsumdifsnd  19873  pgpfaclem1  19995  fincygsubgodd  20026  subdrgint  20718  mplcoe1  21972  mplcoe5  21975  evlslem4  22011  ordtrest2  23119  ufildr  23846  tsmsres  24059  zlmclm  25039  cphipval2  25168  csschl  25303  rrxcph  25319  volinun  25474  uniioombllem4  25514  itg1climres  25642  limcco  25821  vieta1lem2  26246  coseq00topi  26438  tangtx  26441  coskpi  26459  advlog  26590  advlogexp  26591  logtayl  26596  logccv  26599  dvcxp1  26676  dvcncxp1  26679  loglesqrt  26698  ang180lem3  26748  dquart  26790  atans2  26868  basellem8  27025  chtub  27150  bposlem6  27227  lgsquadlem2  27319  logdivsum  27471  log2sumbnd  27482  nodenselem5  27627  oldsuc  27831  precsexlem3  28147  zs12bday  28394  spthispth  29702  ipval3  30689  siii  30833  cm2j  31600  pjssmii  31661  opsqrlem1  32120  hmopidmchi  32131  hmopidmpji  32132  pjcmul1i  32181  mddmd2  32289  cvexchlem  32348  dmdbr6ati  32403  difeq  32498  difuncomp  32533  ffsrn  32711  fzo0opth  32785  symgcom2  33053  cycpmcl  33085  cycpm2tr  33088  rhmimaidl  33397  drngidlhash  33399  1arithidomlem2  33501  qusdimsum  33641  2sqr3minply  33793  cos9thpiminplylem2  33796  zarcmplem  33894  ordtprsuni  33932  ordtrest2NEW  33936  zzsnm  33972  measun  34224  sxbrsigalem2  34299  carsgsigalem  34328  eulerpartlemgu  34390  gsumnunsn  34554  signsplypnf  34563  logdivsqrle  34663  cvmlift2lem12  35358  satf0suc  35420  nepss  35762  fwddifnp1  36207  finxpreclem1  37431  finxpreclem3  37435  poimirlem31  37699  ismblfin  37709  dvtan  37718  itg2addnclem3  37721  dvasin  37752  dvacos  37753  dvreasin  37754  dvreacos  37755  areacirclem1  37756  cnvepima  38373  glbconN  39424  pmodl42N  39898  2polssN  39962  cdleme20j  40365  trlcocnv  40767  trlcone  40775  lclkrlem2c  41556  readvrec2  42402  sn-00idlem3  42441  sn-mul01  42467  selvvvval  42626  diophrw  42800  wopprc  43071  onuniintrab  43267  fsovcnvlem  44054  sineq0ALT  44977  founiiun0  45235  iccdifioo  45563  itgvol0  46014  fourierdlem33  46186  etransclem32  46312  simpcntrab  46916  cycl3grtrilem  47985  gpg3kgrtriexlem2  48123  gpgprismgr4cycllem3  48136  gsumdifsndf  48220  zlmodzxzadd  48397  cosn  48873  oppcendc  49058  resccatlem  49113  resccat  49114  0funcg2  49124  imaf1hom  49148