Theorem 3eqtr4g 2223

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3eqtr4g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4g.2	⊢ 𝐶 = 𝐴
3eqtr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3eqtr4g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	syl5eq 2210	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2216	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  rabbidva2  2712  rabeqf  2715  csbeq1  3047  csbeq2  3068  csbeq2d  3069  csbnestgf  3096  difeq1  3232  difeq2  3233  uneq2  3269  ineq2  3316  dfrab3ss  3399  ifeq1  3522  ifeq2  3523  ifbi  3539  pweq  3561  sneq  3586  csbsng  3636  rabsn  3642  preq1  3652  preq2  3653  tpeq1  3661  tpeq2  3662  tpeq3  3663  prprc1  3683  opeq1  3757  opeq2  3758  oteq1  3766  oteq2  3767  oteq3  3768  csbunig  3796  unieq  3797  inteq  3826  iineq1  3879  iineq2  3882  dfiin2g  3898  iinrabm  3927  iinin1m  3934  iinxprg  3939  opabbid  4046  mpteq12f  4061  suceq  4379  xpeq1  4617  xpeq2  4618  csbxpg  4684  csbdmg  4797  rneq  4830  reseq1  4877  reseq2  4878  csbresg  4886  resindm  4925  resmpt  4931  resmptf  4933  imaeq1  4940  imaeq2  4941  mptcnv  5005  csbrng  5064  dmpropg  5075  rnpropg  5082  cores  5106  cores2  5115  xpcom  5149  iotaeq  5160  iotabi  5161  fntpg  5243  funimaexg  5271  fveq1  5484  fveq2  5485  fvres  5509  csbfv12g  5521  fnimapr  5545  fndmin  5591  fprg  5667  fsnunfv  5685  fsnunres  5686  fliftf  5766  isoini2  5786  riotaeqdv  5798  riotabidv  5799  riotauni  5803  riotabidva  5813  snriota  5826  oveq  5847  oveq1  5848  oveq2  5849  oprabbid  5891  mpoeq123  5897  mpoeq123dva  5899  mpoeq3dva  5902  resmpo  5936  ovres  5977  f1ocnvd  6039  ofeq  6051  ofreq  6052  f1od2  6199  ovtposg  6223  recseq  6270  tfr2a  6285  rdgeq1  6335  rdgeq2  6336  freceq1  6356  freceq2  6357  eceq1  6532  eceq2  6534  qseq1  6545  qseq2  6546  uniqs  6555  ecinxp  6572  qsinxp  6573  erovlem  6589  ixpeq1  6671  supeq1  6947  supeq2  6950  supeq3  6951  supeq123d  6952  infeq1  6972  infeq2  6975  infeq3  6976  infeq123d  6977  infisoti  6993  djueq12  7000  addpiord  7253  mulpiord  7254  00sr  7706  negeq  8087  csbnegg  8092  negsubdi  8150  mulneg1  8289  deceq1  9322  deceq2  9323  xnegeq  9759  fseq1p1m1  10025  frec2uzsucd  10332  frec2uzrdg  10340  frecuzrdgsuc  10345  frecuzrdgg  10347  frecuzrdgsuctlem  10354  seqeq1  10379  seqeq2  10380  seqeq3  10381  seqvalcd  10390  seq3f1olemp  10433  hashprg  10717  shftdm  10760  resqrexlemfp1  10947  negfi  11165  sumeq1  11292  sumeq2  11296  zsumdc  11321  isumss2  11330  fsumsplitsnun  11356  isumclim3  11360  fisumcom2  11375  isumshft  11427  prodeq1f  11489  prodeq2w  11493  prodeq2  11494  zproddc  11516  fprodm1s  11538  fprodp1s  11539  fprodcom2fi  11563  fprodsplitf  11569  ege2le3  11608  efgt1p2  11632  dfphi2  12148  prmdiveq  12164  pceulem  12222  sloteq  12395  setsslid  12440  metreslem  12980  comet  13099  cnmetdval  13129  lgsdi  13538  redcwlpolemeq1  13893