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  2725  rabeqf  2728  csbeq1  3061  csbeq2  3082  csbeq2d  3083  csbnestgf  3110  difeq1  3247  difeq2  3248  uneq2  3284  ineq2  3331  dfrab3ss  3414  ifeq1  3538  ifeq2  3539  ifbi  3555  pweq  3579  sneq  3604  csbsng  3654  rabsn  3660  preq1  3670  preq2  3671  tpeq1  3679  tpeq2  3680  tpeq3  3681  prprc1  3701  opeq1  3779  opeq2  3780  oteq1  3788  oteq2  3789  oteq3  3790  csbunig  3818  unieq  3819  inteq  3848  iineq1  3901  iineq2  3904  dfiin2g  3920  iinrabm  3950  iinin1m  3957  iinxprg  3962  opabbid  4069  mpteq12f  4084  suceq  4403  xpeq1  4641  xpeq2  4642  csbxpg  4708  csbdmg  4822  rneq  4855  reseq1  4902  reseq2  4903  csbresg  4911  resindm  4950  resmpt  4956  resmptf  4958  imaeq1  4966  imaeq2  4967  mptcnv  5032  csbrng  5091  dmpropg  5102  rnpropg  5109  cores  5133  cores2  5142  xpcom  5176  iotaeq  5187  iotabi  5188  fntpg  5273  funimaexg  5301  fveq1  5515  fveq2  5516  fvres  5540  csbfv12g  5552  fnimapr  5577  fndmin  5624  fprg  5700  fsnunfv  5718  fsnunres  5719  fliftf  5800  isoini2  5820  riotaeqdv  5832  riotabidv  5833  riotauni  5837  riotabidva  5847  snriota  5860  oveq  5881  oveq1  5882  oveq2  5883  oprabbid  5928  mpoeq123  5934  mpoeq123dva  5936  mpoeq3dva  5939  resmpo  5973  ovres  6014  f1ocnvd  6073  ofeq  6085  ofreq  6086  f1od2  6236  ovtposg  6260  recseq  6307  tfr2a  6322  rdgeq1  6372  rdgeq2  6373  freceq1  6393  freceq2  6394  eceq1  6570  eceq2  6572  qseq1  6583  qseq2  6584  uniqs  6593  ecinxp  6610  qsinxp  6611  erovlem  6627  ixpeq1  6709  supeq1  6985  supeq2  6988  supeq3  6989  supeq123d  6990  infeq1  7010  infeq2  7013  infeq3  7014  infeq123d  7015  infisoti  7031  djueq12  7038  addpiord  7315  mulpiord  7316  00sr  7768  negeq  8150  csbnegg  8155  negsubdi  8213  mulneg1  8352  deceq1  9388  deceq2  9389  xnegeq  9827  fseq1p1m1  10094  frec2uzsucd  10401  frec2uzrdg  10409  frecuzrdgsuc  10414  frecuzrdgg  10416  frecuzrdgsuctlem  10423  seqeq1  10448  seqeq2  10449  seqeq3  10450  seqvalcd  10459  seq3f1olemp  10502  hashprg  10788  shftdm  10831  resqrexlemfp1  11018  negfi  11236  sumeq1  11363  sumeq2  11367  zsumdc  11392  isumss2  11401  fsumsplitsnun  11427  isumclim3  11431  fisumcom2  11446  isumshft  11498  prodeq1f  11560  prodeq2w  11564  prodeq2  11565  zproddc  11587  fprodm1s  11609  fprodp1s  11610  fprodcom2fi  11634  fprodsplitf  11640  ege2le3  11679  efgt1p2  11703  dfphi2  12220  prmdiveq  12236  pceulem  12294  sloteq  12467  setsslid  12513  ressval2  12526  ringidvalg  13144  metreslem  13883  comet  14002  cnmetdval  14032  lgsdi  14441  lgseisenlem2  14454  redcwlpolemeq1  14805