Theorem eqtr4d 2075

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr4d.1	|- ( ph -> A = B )
eqtr4d.2	|- ( ph -> C = B )

Assertion

Ref	Expression
eqtr4d	|- ( ph -> A = C )

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 |- ( ph -> A = B )
2		eqtr4d.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2045	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2072	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtr2d  2078  3eqtr2rd  2079  3eqtr4d  2082  3eqtr4rd  2083  3eqtr4a  2098  sbnfc2  2906  onsucuni2  4288  relop  4486  riinint  4593  iotauni  4879  fniinfv  5231  fsn2  5337  fmptapd  5354  fconst2g  5376  fniunfv  5401  ofres  5725  ofco  5729  frecsuclem2  5989  frecrdg  5992  oasuc  6044  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  uniqs2  6166  en1bg  6280  fundmen  6286  phplem4dom  6324  addcmpblnq  6465  distrnqg  6485  ltexnqq  6506  addcmpblnq0  6541  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  nq0a0  6555  nnanq0  6556  distrnq0  6557  prarloclemlo  6592  prarloclemcalc  6600  genpassl  6622  genpassu  6623  ltsosr  6849  0idsr  6852  1idsr  6853  mulextsr1lem  6864  cnegex  7189  subsub3  7243  subadd4  7255  mulneg12  7394  mulsub  7398  apreap  7578  cru  7593  recextlem1  7632  cju  7913  halfaddsub  8159  nn0supp  8234  nneo  8341  zeo2  8344  uzin  8505  iccf1o  8872  fzsuc2  8941  flqeqceilz  9160  zmod1congr  9183  frec2uzrdg  9195  iseqss  9226  iseqfveq2  9228  iseqsplit  9238  iseqdistr  9249  iser0f  9251  expp1  9262  mulexp  9294  mulexpzap  9295  expadd  9297  expaddzap  9299  expmul  9300  expmulzap  9301  expsubap  9302  expdivap  9305  subsq  9358  binom3  9366  bernneq  9369  shftval2  9427  shftval4  9429  crre  9457  remim  9460  remullem  9471  cjexp  9493  cnrecnv  9510  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnm  9616  rsqrmo  9625  abscj  9650  absid  9669  absre  9673  recvalap  9693  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  climcvg1nlem  9868  sqrt2irr  9878  ialgrp1  9885