Theorem 3eqtr4g 2228

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  rabbidva2  2717  rabeqf  2720  csbeq1  3052  csbeq2  3073  csbeq2d  3074  csbnestgf  3101  difeq1  3238  difeq2  3239  uneq2  3275  ineq2  3322  dfrab3ss  3405  ifeq1  3529  ifeq2  3530  ifbi  3546  pweq  3569  sneq  3594  csbsng  3644  rabsn  3650  preq1  3660  preq2  3661  tpeq1  3669  tpeq2  3670  tpeq3  3671  prprc1  3691  opeq1  3765  opeq2  3766  oteq1  3774  oteq2  3775  oteq3  3776  csbunig  3804  unieq  3805  inteq  3834  iineq1  3887  iineq2  3890  dfiin2g  3906  iinrabm  3935  iinin1m  3942  iinxprg  3947  opabbid  4054  mpteq12f  4069  suceq  4387  xpeq1  4625  xpeq2  4626  csbxpg  4692  csbdmg  4805  rneq  4838  reseq1  4885  reseq2  4886  csbresg  4894  resindm  4933  resmpt  4939  resmptf  4941  imaeq1  4948  imaeq2  4949  mptcnv  5013  csbrng  5072  dmpropg  5083  rnpropg  5090  cores  5114  cores2  5123  xpcom  5157  iotaeq  5168  iotabi  5169  fntpg  5254  funimaexg  5282  fveq1  5495  fveq2  5496  fvres  5520  csbfv12g  5532  fnimapr  5556  fndmin  5603  fprg  5679  fsnunfv  5697  fsnunres  5698  fliftf  5778  isoini2  5798  riotaeqdv  5810  riotabidv  5811  riotauni  5815  riotabidva  5825  snriota  5838  oveq  5859  oveq1  5860  oveq2  5861  oprabbid  5906  mpoeq123  5912  mpoeq123dva  5914  mpoeq3dva  5917  resmpo  5951  ovres  5992  f1ocnvd  6051  ofeq  6063  ofreq  6064  f1od2  6214  ovtposg  6238  recseq  6285  tfr2a  6300  rdgeq1  6350  rdgeq2  6351  freceq1  6371  freceq2  6372  eceq1  6548  eceq2  6550  qseq1  6561  qseq2  6562  uniqs  6571  ecinxp  6588  qsinxp  6589  erovlem  6605  ixpeq1  6687  supeq1  6963  supeq2  6966  supeq3  6967  supeq123d  6968  infeq1  6988  infeq2  6991  infeq3  6992  infeq123d  6993  infisoti  7009  djueq12  7016  addpiord  7278  mulpiord  7279  00sr  7731  negeq  8112  csbnegg  8117  negsubdi  8175  mulneg1  8314  deceq1  9347  deceq2  9348  xnegeq  9784  fseq1p1m1  10050  frec2uzsucd  10357  frec2uzrdg  10365  frecuzrdgsuc  10370  frecuzrdgg  10372  frecuzrdgsuctlem  10379  seqeq1  10404  seqeq2  10405  seqeq3  10406  seqvalcd  10415  seq3f1olemp  10458  hashprg  10743  shftdm  10786  resqrexlemfp1  10973  negfi  11191  sumeq1  11318  sumeq2  11322  zsumdc  11347  isumss2  11356  fsumsplitsnun  11382  isumclim3  11386  fisumcom2  11401  isumshft  11453  prodeq1f  11515  prodeq2w  11519  prodeq2  11520  zproddc  11542  fprodm1s  11564  fprodp1s  11565  fprodcom2fi  11589  fprodsplitf  11595  ege2le3  11634  efgt1p2  11658  dfphi2  12174  prmdiveq  12190  pceulem  12248  sloteq  12421  setsslid  12466  metreslem  13174  comet  13293  cnmetdval  13323  lgsdi  13732  redcwlpolemeq1  14086