Theorem 3eqtr4g 2198

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

Syntax hints:   → wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  rabbidva2  2676  rabeqf  2679  csbeq1  3010  csbeq2  3031  csbeq2d  3032  csbnestgf  3057  difeq1  3192  difeq2  3193  uneq2  3229  ineq2  3276  dfrab3ss  3359  ifeq1  3482  ifeq2  3483  ifbi  3497  pweq  3518  sneq  3543  csbsng  3592  rabsn  3598  preq1  3608  preq2  3609  tpeq1  3617  tpeq2  3618  tpeq3  3619  prprc1  3639  opeq1  3713  opeq2  3714  oteq1  3722  oteq2  3723  oteq3  3724  csbunig  3752  unieq  3753  inteq  3782  iineq1  3835  iineq2  3838  dfiin2g  3854  iinrabm  3883  iinin1m  3890  iinxprg  3895  opabbid  4001  mpteq12f  4016  suceq  4332  xpeq1  4561  xpeq2  4562  csbxpg  4628  csbdmg  4741  rneq  4774  reseq1  4821  reseq2  4822  csbresg  4830  resindm  4869  resmpt  4875  resmptf  4877  imaeq1  4884  imaeq2  4885  mptcnv  4949  csbrng  5008  dmpropg  5019  rnpropg  5026  cores  5050  cores2  5059  xpcom  5093  iotaeq  5104  iotabi  5105  fntpg  5187  funimaexg  5215  fveq1  5428  fveq2  5429  fvres  5453  csbfv12g  5465  fnimapr  5489  fndmin  5535  fprg  5611  fsnunfv  5629  fsnunres  5630  fliftf  5708  isoini2  5728  riotaeqdv  5739  riotabidv  5740  riotauni  5744  riotabidva  5754  snriota  5767  oveq  5788  oveq1  5789  oveq2  5790  oprabbid  5832  mpoeq123  5838  mpoeq123dva  5840  mpoeq3dva  5843  resmpo  5877  ovres  5918  f1ocnvd  5980  ofeq  5992  ofreq  5993  f1od2  6140  ovtposg  6164  recseq  6211  tfr2a  6226  rdgeq1  6276  rdgeq2  6277  freceq1  6297  freceq2  6298  eceq1  6472  eceq2  6474  qseq1  6485  qseq2  6486  uniqs  6495  ecinxp  6512  qsinxp  6513  erovlem  6529  ixpeq1  6611  supeq1  6881  supeq2  6884  supeq3  6885  supeq123d  6886  infeq1  6906  infeq2  6909  infeq3  6910  infeq123d  6911  infisoti  6927  djueq12  6932  addpiord  7148  mulpiord  7149  00sr  7601  negeq  7979  csbnegg  7984  negsubdi  8042  mulneg1  8181  deceq1  9210  deceq2  9211  xnegeq  9640  fseq1p1m1  9905  frec2uzsucd  10205  frec2uzrdg  10213  frecuzrdgsuc  10218  frecuzrdgg  10220  frecuzrdgsuctlem  10227  seqeq1  10252  seqeq2  10253  seqeq3  10254  seqvalcd  10263  seq3f1olemp  10306  hashprg  10586  shftdm  10626  resqrexlemfp1  10813  negfi  11031  sumeq1  11156  sumeq2  11160  zsumdc  11185  isumss2  11194  fsumsplitsnun  11220  isumclim3  11224  fisumcom2  11239  isumshft  11291  prodeq1f  11353  prodeq2w  11357  prodeq2  11358  zproddc  11380  ege2le3  11414  efgt1p2  11438  dfphi2  11932  sloteq  12003  setsslid  12048  metreslem  12588  comet  12707  cnmetdval  12737  redcwlpolemeq1  13421