Theorem eqtr3di 2787

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

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

This theorem is referenced by:  resdmdfsn  5988  f0dom0  6716  f1o00  6807  fmpt  7054  fmptsn  7113  fninfp  7120  uniordint  7746  fsuppeq  8116  fsuppeqg  8117  mapsnd  8825  sbthlem4  9019  sbthlem6  9021  findcard2s  9091  ssfi  9098  elfiun  9334  cnfcom2  9612  rankxplim3  9794  rankxpsuc  9795  pm54.43  9914  axdc3lem4  10364  gruun  10718  recmulnq  10876  reclem3pr  10961  xrmineq  13121  xadddi2  13238  iooval2  13320  hashsng  14320  hashfun  14388  hashbc  14404  swrds2m  14892  isumclim3  15710  isummulc2  15713  iprodclim3  15954  bpolydiflem  16008  bpoly4  16013  fprodefsum  16049  ruclem4  16190  bitsshft  16433  phimullem  16738  pythagtriplem1  16776  1arithlem4  16886  fsets  17128  topnid  17387  submefmnd  18852  pgrpsubgsymg  19373  odhash  19538  gsumzf1o  19876  gsumdifsnd  19925  pgpfaclem1  20047  fincygsubgodd  20078  subdrgint  20769  mplcoe1  22024  mplcoe5  22027  evlslem4  22063  ordtrest2  23178  ufildr  23905  tsmsres  24118  zlmclm  25088  cphipval2  25217  csschl  25352  rrxcph  25368  volinun  25522  uniioombllem4  25562  itg1climres  25690  limcco  25869  vieta1lem2  26290  coseq00topi  26482  tangtx  26485  coskpi  26503  advlog  26634  advlogexp  26635  logtayl  26640  logccv  26643  dvcxp1  26720  dvcncxp1  26723  loglesqrt  26742  ang180lem3  26792  dquart  26834  atans2  26912  basellem8  27069  chtub  27194  bposlem6  27271  lgsquadlem2  27363  logdivsum  27515  log2sumbnd  27526  nodenselem5  27671  oldsuc  27897  precsexlem3  28220  spthispth  29812  ipval3  30800  siii  30944  cm2j  31711  pjssmii  31772  opsqrlem1  32231  hmopidmchi  32242  hmopidmpji  32243  pjcmul1i  32292  mddmd2  32400  cvexchlem  32459  dmdbr6ati  32514  difeq  32608  difuncomp  32643  ffsrn  32821  fzo0opth  32896  symgcom2  33165  cycpmcl  33197  cycpm2tr  33200  rhmimaidl  33512  drngidlhash  33514  1arithidomlem2  33616  qusdimsum  33793  2sqr3minply  33945  cos9thpiminplylem2  33948  zarcmplem  34046  ordtprsuni  34084  ordtrest2NEW  34088  zzsnm  34124  measun  34376  sxbrsigalem2  34451  carsgsigalem  34480  eulerpartlemgu  34542  gsumnunsn  34706  signsplypnf  34715  logdivsqrle  34815  cvmlift2lem12  35517  satf0suc  35579  nepss  35921  fwddifnp1  36368  finxpreclem1  37716  finxpreclem3  37720  poimirlem31  37983  ismblfin  37993  dvtan  38002  itg2addnclem3  38005  dvasin  38036  dvacos  38037  dvreasin  38038  dvreacos  38039  areacirclem1  38040  cnvepima  38669  disjimeceqim  39136  glbconN  39834  pmodl42N  40308  2polssN  40372  cdleme20j  40775  trlcocnv  41177  trlcone  41185  lclkrlem2c  41966  readvrec2  42804  sn-00idlem3  42843  sn-mul01  42869  selvvvval  43029  diophrw  43202  wopprc  43473  onuniintrab  43669  fsovcnvlem  44455  sineq0ALT  45378  founiiun0  45635  iccdifioo  45960  itgvol0  46411  fourierdlem33  46583  etransclem32  46709  simpcntrab  47313  chnsubseqwl  47322  cycl3grtrilem  48419  gpg3kgrtriexlem2  48557  gpgprismgr4cycllem3  48570  gsumdifsndf  48654  zlmodzxzadd  48831  cosn  49306  oppcendc  49490  resccatlem  49545  resccat  49546  0funcg2  49556  imaf1hom  49580