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  5990  f0dom0  6718  f1o00  6809  fmpt  7056  fmptsn  7115  fninfp  7122  uniordint  7748  fsuppeq  8118  fsuppeqg  8119  mapsnd  8827  sbthlem4  9021  sbthlem6  9023  findcard2s  9093  ssfi  9100  elfiun  9336  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  20771  mplcoe1  22025  mplcoe5  22028  evlslem4  22064  ordtrest2  23179  ufildr  23906  tsmsres  24119  zlmclm  25089  cphipval2  25218  csschl  25353  rrxcph  25369  volinun  25523  uniioombllem4  25563  itg1climres  25691  limcco  25870  vieta1lem2  26288  coseq00topi  26479  tangtx  26482  coskpi  26500  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvcncxp1  26720  loglesqrt  26738  ang180lem3  26788  dquart  26830  atans2  26908  basellem8  27065  chtub  27189  bposlem6  27266  lgsquadlem2  27358  logdivsum  27510  log2sumbnd  27521  nodenselem5  27666  oldsuc  27892  precsexlem3  28215  spthispth  29807  ipval3  30795  siii  30939  cm2j  31706  pjssmii  31767  opsqrlem1  32226  hmopidmchi  32237  hmopidmpji  32238  pjcmul1i  32287  mddmd2  32395  cvexchlem  32454  dmdbr6ati  32509  difeq  32603  difuncomp  32638  ffsrn  32816  fzo0opth  32891  symgcom2  33160  cycpmcl  33192  cycpm2tr  33195  rhmimaidl  33507  drngidlhash  33509  1arithidomlem2  33611  qusdimsum  33788  2sqr3minply  33940  cos9thpiminplylem2  33943  zarcmplem  34041  ordtprsuni  34079  ordtrest2NEW  34083  zzsnm  34119  measun  34371  sxbrsigalem2  34446  carsgsigalem  34475  eulerpartlemgu  34537  gsumnunsn  34701  signsplypnf  34710  logdivsqrle  34810  cvmlift2lem12  35512  satf0suc  35574  nepss  35916  fwddifnp1  36363  finxpreclem1  37719  finxpreclem3  37723  poimirlem31  37986  ismblfin  37996  dvtan  38005  itg2addnclem3  38008  dvasin  38039  dvacos  38040  dvreasin  38041  dvreacos  38042  areacirclem1  38043  cnvepima  38672  disjimeceqim  39139  glbconN  39837  pmodl42N  40311  2polssN  40375  cdleme20j  40778  trlcocnv  41180  trlcone  41188  lclkrlem2c  41969  readvrec2  42807  sn-00idlem3  42846  sn-mul01  42872  selvvvval  43032  diophrw  43205  wopprc  43476  onuniintrab  43672  fsovcnvlem  44458  sineq0ALT  45381  founiiun0  45638  iccdifioo  45963  itgvol0  46414  fourierdlem33  46586  etransclem32  46712  simpcntrab  47316  chnsubseqwl  47325  sin5tlem1  47337  cycl3grtrilem  48434  gpg3kgrtriexlem2  48572  gpgprismgr4cycllem3  48585  gsumdifsndf  48669  zlmodzxzadd  48846  cosn  49321  oppcendc  49505  resccatlem  49560  resccat  49561  0funcg2  49571  imaf1hom  49595