Theorem eqtr3di 2794

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  resdmdfsn  5930  f0dom0  6642  f1o00  6734  fmpt  6966  fmptsn  7021  fninfp  7028  uniordint  7628  frnsuppeq  7962  frnsuppeqg  7963  mapsnd  8632  sbthlem4  8826  sbthlem6  8828  findcard2s  8910  ssfi  8918  elfiun  9119  cnfcom2  9390  rankxplim3  9570  rankxpsuc  9571  pm54.43  9690  axdc3lem4  10140  gruun  10493  recmulnq  10651  reclem3pr  10736  xrmineq  12843  xadddi2  12960  iooval2  13041  hashsng  14012  hashfun  14080  hashbc  14093  swrds2m  14582  isumclim3  15399  isummulc2  15402  iprodclim3  15638  bpolydiflem  15692  bpoly4  15697  fprodefsum  15732  ruclem4  15871  bitsshft  16110  phimullem  16408  pythagtriplem1  16445  1arithlem4  16555  fsets  16798  topnid  17063  submefmnd  18449  pgrpsubgsymg  18932  odhash  19094  gsumzf1o  19428  gsumdifsnd  19477  pgpfaclem1  19599  fincygsubgodd  19630  subdrgint  19986  mplcoe1  21148  mplcoe5  21151  evlslem4  21194  ordtrest2  22263  ufildr  22990  tsmsres  23203  zlmclm  24181  cphipval2  24310  csschl  24445  rrxcph  24461  volinun  24615  uniioombllem4  24655  itg1climres  24784  limcco  24962  vieta1lem2  25376  coseq00topi  25564  tangtx  25567  coskpi  25584  advlog  25714  advlogexp  25715  logtayl  25720  logccv  25723  dvcxp1  25798  dvcncxp1  25801  loglesqrt  25816  ang180lem3  25866  dquart  25908  atans2  25986  basellem8  26142  chtub  26265  bposlem6  26342  lgsquadlem2  26434  logdivsum  26586  log2sumbnd  26597  spthispth  27995  ipval3  28972  siii  29116  cm2j  29883  pjssmii  29944  opsqrlem1  30403  hmopidmchi  30414  hmopidmpji  30415  pjcmul1i  30464  mddmd2  30572  cvexchlem  30631  dmdbr6ati  30686  difeq  30766  difuncomp  30794  ffsrn  30966  symgcom2  31255  cycpmcl  31285  cycpm2tr  31288  rhmimaidl  31511  qusdimsum  31611  zarcmplem  31733  ordtprsuni  31771  ordtrest2NEW  31775  zzsnm  31811  measun  32079  sxbrsigalem2  32153  carsgsigalem  32182  eulerpartlemgu  32244  gsumnunsn  32420  signsplypnf  32429  logdivsqrle  32530  cvmlift2lem12  33176  satf0suc  33238  nepss  33564  nodenselem5  33818  oldsuc  33995  fwddifnp1  34394  finxpreclem1  35487  finxpreclem3  35491  poimirlem31  35735  ismblfin  35745  dvtan  35754  itg2addnclem3  35757  dvasin  35788  dvacos  35789  dvreasin  35790  dvreacos  35791  areacirclem1  35792  cnvepima  36399  glbconN  37318  pmodl42N  37792  2polssN  37856  cdleme20j  38259  trlcocnv  38661  trlcone  38669  lclkrlem2c  39450  sn-mul01  40328  diophrw  40497  wopprc  40768  fsovcnvlem  41510  sineq0ALT  42446  founiiun0  42617  iccdifioo  42943  itgvol0  43399  fourierdlem33  43571  etransclem32  43697  simpcntrab  44273  gsumdifsndf  45263  zlmodzxzadd  45582