Theorem 3eqtr4g 2292

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  rabbidva2  2799  rabeqf  2805  csbeq1  3143  csbeq2  3164  csbeq2d  3165  csbnestgf  3193  difeq1  3332  difeq2  3333  uneq2  3369  ineq2  3418  dfrab3ss  3501  ifeq1  3627  ifeq2  3628  ifbi  3645  pweq  3674  sneq  3702  csbsng  3752  rabsn  3758  preq1  3770  preq2  3771  tpeq1  3779  tpeq2  3780  tpeq3  3781  prprc1  3802  opeq1  3885  opeq2  3886  oteq1  3894  oteq2  3895  oteq3  3896  csbunig  3924  unieq  3925  inteq  3954  iineq1  4007  iineq2  4010  dfiin2g  4026  iinrabm  4056  iinin1m  4063  iinxprg  4068  opabbid  4177  mpteq12f  4192  suceq  4525  xpeq1  4765  xpeq2  4766  csbxpg  4833  csbdmg  4952  rneq  4986  reseq1  5034  reseq2  5035  csbresg  5043  resindm  5082  resmpt  5088  resmptf  5090  imaeq1  5098  imaeq2  5099  mptcnv  5167  csbrng  5226  dmpropg  5237  rnpropg  5244  cores  5268  cores2  5277  xpcom  5311  iotaeq  5323  iotabi  5324  fntpg  5414  funimaexg  5442  fveq1  5671  fveq2  5672  fvres  5696  csbfv12g  5712  fnimapr  5739  fndmin  5787  fprg  5869  fsnunfv  5887  fsnunres  5888  fliftf  5974  isoini2  5994  riotaeqdv  6006  riotabidv  6007  riotauni  6012  riotabidva  6023  snriota  6037  oveq  6058  oveq1  6059  oveq2  6060  oprabbid  6108  mpoeq123  6114  mpoeq123dva  6116  mpoeq3dva  6119  resmpo  6153  ovres  6196  f1ocnvd  6259  ofeqd  6270  ofeq  6271  ofreq  6272  f1od2  6433  ovtposg  6492  recseq  6539  tfr2a  6554  rdgeq1  6604  rdgeq2  6605  freceq1  6625  freceq2  6626  eceq1  6804  eceq2  6806  qseq1  6819  qseq2  6820  uniqs  6829  ecinxp  6846  qsinxp  6847  erovlem  6863  ixpeq1  6946  supeq1  7279  supeq2  7282  supeq3  7283  supeq123d  7284  infeq1  7304  infeq2  7307  infeq3  7308  infeq123d  7309  infisoti  7325  djueq12  7332  acneq  7511  addpiord  7633  mulpiord  7634  00sr  8086  negeq  8468  csbnegg  8473  negsubdi  8531  mulneg1  8670  deceq1  9716  deceq2  9717  xnegeq  10163  fseq1p1m1  10432  frec2uzsucd  10767  frec2uzrdg  10775  frecuzrdgsuc  10780  frecuzrdgg  10782  frecuzrdgsuctlem  10789  seqeq1  10816  seqeq2  10817  seqeq3  10818  seqvalcd  10827  seq3f1olemp  10881  hashprg  11177  s1eq  11311  s1prc  11315  s2eqd  11466  s3eqd  11467  s4eqd  11468  s5eqd  11469  s6eqd  11470  s7eqd  11471  s8eqd  11472  shftdm  11511  resqrexlemfp1  11698  negfi  11917  sumeq1  12044  sumeq2  12048  zsumdc  12074  isumss2  12083  fsumsplitsnun  12109  isumclim3  12113  fisumcom2  12128  isumshft  12180  prodeq1f  12242  prodeq2w  12246  prodeq2  12247  zproddc  12269  fprodm1s  12291  fprodp1s  12292  fprodcom2fi  12316  fprodsplitf  12322  ege2le3  12361  efgt1p2  12385  dfphi2  12921  prmdiveq  12937  pceulem  12996  sloteq  13234  setsslid  13280  ressval2  13296  ecqusaddd  13972  ringidvalg  14122  zrhpropd  14791  metreslem  15262  comet  15381  cnmetdval  15411  dvmptfsum  15607  dvply1  15647  lgsdi  15927  lgseisenlem2  15961  lgsquadlem3  15969  uhgrvtxedgiedgb  16155  usgredg2v  16236  depindlem1  16518  redcwlpolemeq1  16856  gfsumz  16886