Theorem 3eqtr4g 2235

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	eqtrid 2222	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2228	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  rabbidva2  2724  rabeqf  2727  csbeq1  3060  csbeq2  3081  csbeq2d  3082  csbnestgf  3109  difeq1  3246  difeq2  3247  uneq2  3283  ineq2  3330  dfrab3ss  3413  ifeq1  3537  ifeq2  3538  ifbi  3554  pweq  3578  sneq  3603  csbsng  3653  rabsn  3659  preq1  3669  preq2  3670  tpeq1  3678  tpeq2  3679  tpeq3  3680  prprc1  3700  opeq1  3778  opeq2  3779  oteq1  3787  oteq2  3788  oteq3  3789  csbunig  3817  unieq  3818  inteq  3847  iineq1  3900  iineq2  3903  dfiin2g  3919  iinrabm  3949  iinin1m  3956  iinxprg  3961  opabbid  4068  mpteq12f  4083  suceq  4402  xpeq1  4640  xpeq2  4641  csbxpg  4707  csbdmg  4821  rneq  4854  reseq1  4901  reseq2  4902  csbresg  4910  resindm  4949  resmpt  4955  resmptf  4957  imaeq1  4965  imaeq2  4966  mptcnv  5031  csbrng  5090  dmpropg  5101  rnpropg  5108  cores  5132  cores2  5141  xpcom  5175  iotaeq  5186  iotabi  5187  fntpg  5272  funimaexg  5300  fveq1  5514  fveq2  5515  fvres  5539  csbfv12g  5551  fnimapr  5576  fndmin  5623  fprg  5699  fsnunfv  5717  fsnunres  5718  fliftf  5799  isoini2  5819  riotaeqdv  5831  riotabidv  5832  riotauni  5836  riotabidva  5846  snriota  5859  oveq  5880  oveq1  5881  oveq2  5882  oprabbid  5927  mpoeq123  5933  mpoeq123dva  5935  mpoeq3dva  5938  resmpo  5972  ovres  6013  f1ocnvd  6072  ofeq  6084  ofreq  6085  f1od2  6235  ovtposg  6259  recseq  6306  tfr2a  6321  rdgeq1  6371  rdgeq2  6372  freceq1  6392  freceq2  6393  eceq1  6569  eceq2  6571  qseq1  6582  qseq2  6583  uniqs  6592  ecinxp  6609  qsinxp  6610  erovlem  6626  ixpeq1  6708  supeq1  6984  supeq2  6987  supeq3  6988  supeq123d  6989  infeq1  7009  infeq2  7012  infeq3  7013  infeq123d  7014  infisoti  7030  djueq12  7037  addpiord  7314  mulpiord  7315  00sr  7767  negeq  8149  csbnegg  8154  negsubdi  8212  mulneg1  8351  deceq1  9387  deceq2  9388  xnegeq  9826  fseq1p1m1  10093  frec2uzsucd  10400  frec2uzrdg  10408  frecuzrdgsuc  10413  frecuzrdgg  10415  frecuzrdgsuctlem  10422  seqeq1  10447  seqeq2  10448  seqeq3  10449  seqvalcd  10458  seq3f1olemp  10501  hashprg  10787  shftdm  10830  resqrexlemfp1  11017  negfi  11235  sumeq1  11362  sumeq2  11366  zsumdc  11391  isumss2  11400  fsumsplitsnun  11426  isumclim3  11430  fisumcom2  11445  isumshft  11497  prodeq1f  11559  prodeq2w  11563  prodeq2  11564  zproddc  11586  fprodm1s  11608  fprodp1s  11609  fprodcom2fi  11633  fprodsplitf  11639  ege2le3  11678  efgt1p2  11702  dfphi2  12219  prmdiveq  12235  pceulem  12293  sloteq  12466  setsslid  12512  ressval2  12525  ringidvalg  13142  metreslem  13850  comet  13969  cnmetdval  13999  lgsdi  14408  lgseisenlem2  14421  redcwlpolemeq1  14772