Theorem eqtr3di 2788

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 2742	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2786	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  resdmdfsn  6032  f0dom0  6776  f1o00  6869  fmpt  7110  fmptsn  7165  fninfp  7172  uniordint  7789  fsuppeq  8160  fsuppeqg  8161  mapsnd  8880  sbthlem4  9086  sbthlem6  9088  findcard2s  9165  ssfi  9173  elfiun  9425  cnfcom2  9697  rankxplim3  9876  rankxpsuc  9877  pm54.43  9996  axdc3lem4  10448  gruun  10801  recmulnq  10959  reclem3pr  11044  xrmineq  13159  xadddi2  13276  iooval2  13357  hashsng  14329  hashfun  14397  hashbc  14412  swrds2m  14892  isumclim3  15705  isummulc2  15708  iprodclim3  15944  bpolydiflem  15998  bpoly4  16003  fprodefsum  16038  ruclem4  16177  bitsshft  16416  phimullem  16712  pythagtriplem1  16749  1arithlem4  16859  fsets  17102  topnid  17381  submefmnd  18776  pgrpsubgsymg  19277  odhash  19442  gsumzf1o  19780  gsumdifsnd  19829  pgpfaclem1  19951  fincygsubgodd  19982  subdrgint  20419  mplcoe1  21592  mplcoe5  21595  evlslem4  21637  ordtrest2  22708  ufildr  23435  tsmsres  23648  zlmclm  24628  cphipval2  24758  csschl  24893  rrxcph  24909  volinun  25063  uniioombllem4  25103  itg1climres  25232  limcco  25410  vieta1lem2  25824  coseq00topi  26012  tangtx  26015  coskpi  26032  advlog  26162  advlogexp  26163  logtayl  26168  logccv  26171  dvcxp1  26248  dvcncxp1  26251  loglesqrt  26266  ang180lem3  26316  dquart  26358  atans2  26436  basellem8  26592  chtub  26715  bposlem6  26792  lgsquadlem2  26884  logdivsum  27036  log2sumbnd  27047  nodenselem5  27191  oldsuc  27380  precsexlem3  27655  spthispth  28983  ipval3  29962  siii  30106  cm2j  30873  pjssmii  30934  opsqrlem1  31393  hmopidmchi  31404  hmopidmpji  31405  pjcmul1i  31454  mddmd2  31562  cvexchlem  31621  dmdbr6ati  31676  difeq  31756  difuncomp  31785  ffsrn  31954  symgcom2  32245  cycpmcl  32275  cycpm2tr  32278  rhmimaidl  32550  drngidlhash  32552  qusdimsum  32713  zarcmplem  32861  ordtprsuni  32899  ordtrest2NEW  32903  zzsnm  32939  measun  33209  sxbrsigalem2  33285  carsgsigalem  33314  eulerpartlemgu  33376  gsumnunsn  33552  signsplypnf  33561  logdivsqrle  33662  cvmlift2lem12  34305  satf0suc  34367  nepss  34687  fwddifnp1  35137  finxpreclem1  36270  finxpreclem3  36274  poimirlem31  36519  ismblfin  36529  dvtan  36538  itg2addnclem3  36541  dvasin  36572  dvacos  36573  dvreasin  36574  dvreacos  36575  areacirclem1  36576  cnvepima  37206  glbconN  38247  glbconNOLD  38248  pmodl42N  38722  2polssN  38786  cdleme20j  39189  trlcocnv  39591  trlcone  39599  lclkrlem2c  40380  selvvvval  41157  sn-mul01  41298  diophrw  41497  wopprc  41769  onuniintrab  41975  fsovcnvlem  42764  sineq0ALT  43698  founiiun0  43888  iccdifioo  44228  itgvol0  44684  fourierdlem33  44856  etransclem32  44982  simpcntrab  45586  gsumdifsndf  46591  zlmodzxzadd  47034