Theorem eqtr3di 2784

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 2743	. 2 ⊢ 𝐶 = 𝐴
3		eqtr3di.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	eqtr2id 2782	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 2123  ax-ext 2706

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

This theorem is referenced by:  resdmdfsn  5988  f0dom0  6716  f1o00  6807  fmpt  7053  fmptsn  7111  fninfp  7118  uniordint  7744  fsuppeq  8115  fsuppeqg  8116  mapsnd  8822  sbthlem4  9016  sbthlem6  9018  findcard2s  9088  ssfi  9095  elfiun  9331  cnfcom2  9609  rankxplim3  9791  rankxpsuc  9792  pm54.43  9911  axdc3lem4  10361  gruun  10715  recmulnq  10873  reclem3pr  10958  xrmineq  13093  xadddi2  13210  iooval2  13292  hashsng  14290  hashfun  14358  hashbc  14374  swrds2m  14862  isumclim3  15680  isummulc2  15683  iprodclim3  15921  bpolydiflem  15975  bpoly4  15980  fprodefsum  16016  ruclem4  16157  bitsshft  16400  phimullem  16704  pythagtriplem1  16742  1arithlem4  16852  fsets  17094  topnid  17353  submefmnd  18818  pgrpsubgsymg  19336  odhash  19501  gsumzf1o  19839  gsumdifsnd  19888  pgpfaclem1  20010  fincygsubgodd  20041  subdrgint  20734  mplcoe1  21990  mplcoe5  21993  evlslem4  22029  ordtrest2  23146  ufildr  23873  tsmsres  24086  zlmclm  25066  cphipval2  25195  csschl  25330  rrxcph  25346  volinun  25501  uniioombllem4  25541  itg1climres  25669  limcco  25848  vieta1lem2  26273  coseq00topi  26465  tangtx  26468  coskpi  26486  advlog  26617  advlogexp  26618  logtayl  26623  logccv  26626  dvcxp1  26703  dvcncxp1  26706  loglesqrt  26725  ang180lem3  26775  dquart  26817  atans2  26895  basellem8  27052  chtub  27177  bposlem6  27254  lgsquadlem2  27346  logdivsum  27498  log2sumbnd  27509  nodenselem5  27654  oldsuc  27858  precsexlem3  28177  zs12bday  28433  spthispth  29746  ipval3  30733  siii  30877  cm2j  31644  pjssmii  31705  opsqrlem1  32164  hmopidmchi  32175  hmopidmpji  32176  pjcmul1i  32225  mddmd2  32333  cvexchlem  32392  dmdbr6ati  32447  difeq  32542  difuncomp  32577  ffsrn  32756  fzo0opth  32832  symgcom2  33115  cycpmcl  33147  cycpm2tr  33150  rhmimaidl  33462  drngidlhash  33464  1arithidomlem2  33566  qusdimsum  33734  2sqr3minply  33886  cos9thpiminplylem2  33889  zarcmplem  33987  ordtprsuni  34025  ordtrest2NEW  34029  zzsnm  34065  measun  34317  sxbrsigalem2  34392  carsgsigalem  34421  eulerpartlemgu  34483  gsumnunsn  34647  signsplypnf  34656  logdivsqrle  34756  cvmlift2lem12  35457  satf0suc  35519  nepss  35861  fwddifnp1  36308  finxpreclem1  37533  finxpreclem3  37537  poimirlem31  37791  ismblfin  37801  dvtan  37810  itg2addnclem3  37813  dvasin  37844  dvacos  37845  dvreasin  37846  dvreacos  37847  areacirclem1  37848  cnvepima  38469  glbconN  39576  pmodl42N  40050  2polssN  40114  cdleme20j  40517  trlcocnv  40919  trlcone  40927  lclkrlem2c  41708  readvrec2  42558  sn-00idlem3  42597  sn-mul01  42623  selvvvval  42770  diophrw  42943  wopprc  43214  onuniintrab  43410  fsovcnvlem  44196  sineq0ALT  45119  founiiun0  45376  iccdifioo  45703  itgvol0  46154  fourierdlem33  46326  etransclem32  46452  simpcntrab  47056  chnsubseqwl  47065  cycl3grtrilem  48134  gpg3kgrtriexlem2  48272  gpgprismgr4cycllem3  48285  gsumdifsndf  48369  zlmodzxzadd  48546  cosn  49021  oppcendc  49205  resccatlem  49260  resccat  49261  0funcg2  49271  imaf1hom  49295