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  5998  f0dom0  6726  f1o00  6817  fmpt  7064  fmptsn  7123  fninfp  7130  uniordint  7756  fsuppeq  8127  fsuppeqg  8128  mapsnd  8836  sbthlem4  9030  sbthlem6  9032  findcard2s  9102  ssfi  9109  elfiun  9345  cnfcom2  9623  rankxplim3  9805  rankxpsuc  9806  pm54.43  9925  axdc3lem4  10375  gruun  10729  recmulnq  10887  reclem3pr  10972  xrmineq  13107  xadddi2  13224  iooval2  13306  hashsng  14304  hashfun  14372  hashbc  14388  swrds2m  14876  isumclim3  15694  isummulc2  15697  iprodclim3  15935  bpolydiflem  15989  bpoly4  15994  fprodefsum  16030  ruclem4  16171  bitsshft  16414  phimullem  16718  pythagtriplem1  16756  1arithlem4  16866  fsets  17108  topnid  17367  submefmnd  18832  pgrpsubgsymg  19350  odhash  19515  gsumzf1o  19853  gsumdifsnd  19902  pgpfaclem1  20024  fincygsubgodd  20055  subdrgint  20748  mplcoe1  22004  mplcoe5  22007  evlslem4  22043  ordtrest2  23160  ufildr  23887  tsmsres  24100  zlmclm  25080  cphipval2  25209  csschl  25344  rrxcph  25360  volinun  25515  uniioombllem4  25555  itg1climres  25683  limcco  25862  vieta1lem2  26287  coseq00topi  26479  tangtx  26482  coskpi  26500  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvcncxp1  26720  loglesqrt  26739  ang180lem3  26789  dquart  26831  atans2  26909  basellem8  27066  chtub  27191  bposlem6  27268  lgsquadlem2  27360  logdivsum  27512  log2sumbnd  27523  nodenselem5  27668  oldsuc  27894  precsexlem3  28217  spthispth  29809  ipval3  30797  siii  30941  cm2j  31708  pjssmii  31769  opsqrlem1  32228  hmopidmchi  32239  hmopidmpji  32240  pjcmul1i  32289  mddmd2  32397  cvexchlem  32456  dmdbr6ati  32511  difeq  32605  difuncomp  32640  ffsrn  32818  fzo0opth  32894  symgcom2  33178  cycpmcl  33210  cycpm2tr  33213  rhmimaidl  33525  drngidlhash  33527  1arithidomlem2  33629  qusdimsum  33806  2sqr3minply  33958  cos9thpiminplylem2  33961  zarcmplem  34059  ordtprsuni  34097  ordtrest2NEW  34101  zzsnm  34137  measun  34389  sxbrsigalem2  34464  carsgsigalem  34493  eulerpartlemgu  34555  gsumnunsn  34719  signsplypnf  34728  logdivsqrle  34828  cvmlift2lem12  35530  satf0suc  35592  nepss  35934  fwddifnp1  36381  finxpreclem1  37644  finxpreclem3  37648  poimirlem31  37902  ismblfin  37912  dvtan  37921  itg2addnclem3  37924  dvasin  37955  dvacos  37956  dvreasin  37957  dvreacos  37958  areacirclem1  37959  cnvepima  38588  disjimeceqim  39055  glbconN  39753  pmodl42N  40227  2polssN  40291  cdleme20j  40694  trlcocnv  41096  trlcone  41104  lclkrlem2c  41885  readvrec2  42731  sn-00idlem3  42770  sn-mul01  42796  selvvvval  42943  diophrw  43116  wopprc  43387  onuniintrab  43583  fsovcnvlem  44369  sineq0ALT  45292  founiiun0  45549  iccdifioo  45875  itgvol0  46326  fourierdlem33  46498  etransclem32  46624  simpcntrab  47228  chnsubseqwl  47237  cycl3grtrilem  48306  gpg3kgrtriexlem2  48444  gpgprismgr4cycllem3  48457  gsumdifsndf  48541  zlmodzxzadd  48718  cosn  49193  oppcendc  49377  resccatlem  49432  resccat  49433  0funcg2  49443  imaf1hom  49467