Theorem 3eqtr4d 2082

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4d	|- ( ph -> C = D )

Proof of Theorem 3eqtr4d

Step	Hyp	Ref	Expression
1		3eqtr4d.2	. 2 |- ( ph -> C = A )
2		3eqtr4d.3	. . 3 |- ( ph -> D = B )
3		3eqtr4d.1	. . 3 |- ( ph -> A = B )
4	2, 3	eqtr4d 2075	. 2 |- ( ph -> D = A )
5	1, 4	eqtr4d 2075	1 |- ( ph -> C = D )

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:  fnsnfv  5232  fvco2  5242  resfunexg  5382  fcof1  5423  fliftfun  5436  caovdir2d  5677  caov32d  5681  caov31d  5683  caov4d  5685  caovlem2d  5693  caofcom  5734  cnvf1olem  5845  tfrlem1  5923  tfrlemisucaccv  5939  frecrdg  5992  oav2  6043  omv2  6045  omsuc  6051  nnmsucr  6067  ecovicom  6214  ecoviass  6216  ecovidi  6218  carden2bex  6369  addcompig  6427  addasspig  6428  mulcompig  6429  mulasspig  6430  distrpig  6431  addassnqg  6480  addnq0mo  6545  mulnq0mo  6546  nqnq0a  6552  nqnq0m  6553  distrnq0  6557  mulcomnq0  6558  addassnq0  6560  addcmpblnr  6824  mulcmpblnrlemg  6825  addsrmo  6828  mulsrmo  6829  ltsrprg  6832  recexgt0sr  6858  mulgt0sr  6862  mulextsr1lem  6864  addcnsrec  6918  mulcnsrec  6919  pitonnlem2  6923  recidpirqlemcalc  6933  axaddcom  6944  adddir  7018  mul32  7143  mul31  7144  add32  7170  add4  7172  sub32  7245  sub4  7256  subdir  7383  mulneg2  7393  mulreim  7595  apadd1  7599  apneg  7602  divassap  7669  divdirap  7674  divmul13ap  7691  divmul24ap  7692  divdiv32ap  7696  conjmulap  7705  zeo  8343  lincmb01cmp  8871  iccf1o  8872  flhalf  9144  iseqshft2  9232  iseqcaopr3  9240  iseqcaopr  9242  iseqhomo  9248  iseqdistr  9249  expp1  9262  expnegap0  9263  expaddzaplem  9298  expaddzap  9299  expmulzap  9301  sqneg  9313  sqdivap  9318  subsq2  9359  binom2  9362  shftfibg  9421  shftfib  9424  shftval  9426  2shfti  9432  crre  9457  remim  9460  mulreap  9464  reneg  9468  readd  9469  remullem  9471  redivap  9474  imneg  9476  imadd  9477  imdivap  9481  cjcj  9483  cjadd  9484  cjmulrcl  9487  cjneg  9490  imval2  9494  resqrexlemcalc1  9612  absneg  9648  sqabsadd  9653  sqabssub  9654  absmul  9667  absresq  9674  absexp  9675  absexpzap  9676  serif0  9871