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 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

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

This theorem is referenced by:  resdmdfsn  6031  f0dom0  6773  f1o00  6864  fmpt  7111  fmptsn  7170  fninfp  7177  uniordint  7804  fsuppeq  8183  fsuppeqg  8184  mapsnd  8909  sbthlem4  9109  sbthlem6  9111  findcard2s  9188  ssfi  9196  elfiun  9453  cnfcom2  9725  rankxplim3  9904  rankxpsuc  9905  pm54.43  10024  axdc3lem4  10476  gruun  10829  recmulnq  10987  reclem3pr  11072  xrmineq  13205  xadddi2  13322  iooval2  13403  hashsng  14391  hashfun  14459  hashbc  14475  swrds2m  14963  isumclim3  15778  isummulc2  15781  iprodclim3  16019  bpolydiflem  16073  bpoly4  16078  fprodefsum  16114  ruclem4  16253  bitsshft  16495  phimullem  16799  pythagtriplem1  16837  1arithlem4  16947  fsets  17189  topnid  17456  submefmnd  18882  pgrpsubgsymg  19400  odhash  19565  gsumzf1o  19903  gsumdifsnd  19952  pgpfaclem1  20074  fincygsubgodd  20105  subdrgint  20777  mplcoe1  22022  mplcoe5  22025  evlslem4  22067  ordtrest2  23177  ufildr  23904  tsmsres  24117  zlmclm  25100  cphipval2  25230  csschl  25365  rrxcph  25381  volinun  25536  uniioombllem4  25576  itg1climres  25704  limcco  25883  vieta1lem2  26308  coseq00topi  26499  tangtx  26502  coskpi  26520  advlog  26651  advlogexp  26652  logtayl  26657  logccv  26660  dvcxp1  26737  dvcncxp1  26740  loglesqrt  26759  ang180lem3  26809  dquart  26851  atans2  26929  basellem8  27086  chtub  27211  bposlem6  27288  lgsquadlem2  27380  logdivsum  27532  log2sumbnd  27543  nodenselem5  27688  oldsuc  27879  precsexlem3  28188  zs12bday  28379  spthispth  29691  ipval3  30675  siii  30819  cm2j  31586  pjssmii  31647  opsqrlem1  32106  hmopidmchi  32117  hmopidmpji  32118  pjcmul1i  32167  mddmd2  32275  cvexchlem  32334  dmdbr6ati  32389  difeq  32484  difuncomp  32513  ffsrn  32687  fzo0opth  32754  symgcom2  33050  cycpmcl  33082  cycpm2tr  33085  rhmimaidl  33401  drngidlhash  33403  1arithidomlem2  33505  qusdimsum  33620  2sqr3minply  33732  zarcmplem  33821  ordtprsuni  33859  ordtrest2NEW  33863  zzsnm  33899  measun  34153  sxbrsigalem2  34229  carsgsigalem  34258  eulerpartlemgu  34320  gsumnunsn  34497  signsplypnf  34506  logdivsqrle  34606  cvmlift2lem12  35260  satf0suc  35322  nepss  35659  fwddifnp1  36107  finxpreclem1  37331  finxpreclem3  37335  poimirlem31  37599  ismblfin  37609  dvtan  37618  itg2addnclem3  37621  dvasin  37652  dvacos  37653  dvreasin  37654  dvreacos  37655  areacirclem1  37656  cnvepima  38279  glbconN  39319  glbconNOLD  39320  pmodl42N  39794  2polssN  39858  cdleme20j  40261  trlcocnv  40663  trlcone  40671  lclkrlem2c  41452  readvrec2  42336  sn-mul01  42400  selvvvval  42540  diophrw  42715  wopprc  42987  onuniintrab  43183  fsovcnvlem  43971  sineq0ALT  44902  founiiun0  45140  iccdifioo  45473  itgvol0  45928  fourierdlem33  46100  etransclem32  46226  simpcntrab  46830  cycl3grtrilem  47859  gpg3kgrtriexlem2  47986  gsumdifsndf  48043  zlmodzxzadd  48220  cosn  48691  oppcendc  48862  0funcg2  48874