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  3144  csbeq2  3165  csbeq2d  3166  csbnestgf  3194  difeq1  3334  difeq2  3335  uneq2  3371  ineq2  3420  dfrab3ss  3503  ifeq1  3629  ifeq2  3630  ifbi  3647  pweq  3677  sneq  3705  csbsng  3755  rabsn  3761  preq1  3773  preq2  3774  tpeq1  3782  tpeq2  3783  tpeq3  3784  prprc1  3805  opeq1  3888  opeq2  3889  oteq1  3897  oteq2  3898  oteq3  3899  csbunig  3927  unieq  3928  inteq  3957  iineq1  4010  iineq2  4013  dfiin2g  4029  iinrabm  4059  iinin1m  4066  iinxprg  4071  opabbid  4180  mpteq12f  4195  suceq  4528  xpeq1  4768  xpeq2  4769  csbxpg  4836  csbdmg  4955  rneq  4989  reseq1  5037  reseq2  5038  csbresg  5046  resindm  5085  resmpt  5091  resmptf  5093  imaeq1  5101  imaeq2  5102  mptcnv  5170  csbrng  5229  dmpropg  5240  rnpropg  5247  cores  5271  cores2  5280  xpcom  5314  iotaeq  5326  iotabi  5327  fntpg  5417  funimaexg  5445  fveq1  5674  fveq2  5675  fvres  5699  csbfv12g  5715  fnimapr  5742  fndmin  5790  fprg  5872  fsnunfv  5890  fsnunres  5891  fliftf  5978  isoini2  5998  riotaeqdv  6012  riotabidv  6013  riotauni  6018  riotabidva  6029  snriota  6043  oveq  6064  oveq1  6065  oveq2  6066  oprabbid  6114  mpoeq123  6120  mpoeq123dva  6122  mpoeq3dva  6125  resmpo  6159  ovres  6202  f1ocnvd  6265  ofeqd  6277  ofeq  6278  ofreq  6279  f1od2  6444  ovtposg  6503  recseq  6550  tfr2a  6565  rdgeq1  6615  rdgeq2  6616  freceq1  6636  freceq2  6637  eceq1  6815  eceq2  6817  qseq1  6830  qseq2  6831  uniqs  6840  ecinxp  6857  qsinxp  6858  erovlem  6874  ixpeq1  6957  supeq1  7290  supeq2  7293  supeq3  7294  supeq123d  7295  infeq1  7315  infeq2  7318  infeq3  7319  infeq123d  7320  infisoti  7336  djueq12  7343  acneq  7522  addpiord  7647  mulpiord  7648  00sr  8100  negeq  8482  csbnegg  8487  negsubdi  8545  mulneg1  8685  deceq1  9731  deceq2  9732  xnegeq  10179  fseq1p1m1  10450  frec2uzsucd  10787  frec2uzrdg  10795  frecuzrdgsuc  10800  frecuzrdgg  10802  frecuzrdgsuctlem  10809  seqeq1  10836  seqeq2  10837  seqeq3  10838  seqvalcd  10847  seq3f1olemp  10901  hashprg  11198  s1eq  11332  s1prc  11336  s2eqd  11487  s3eqd  11488  s4eqd  11489  s5eqd  11490  s6eqd  11491  s7eqd  11492  s8eqd  11493  shftdm  11532  resqrexlemfp1  11719  negfi  11938  sumeq1  12065  sumeq2  12069  zsumdc  12095  isumss2  12104  fsumsplitsnun  12130  isumclim3  12134  fisumcom2  12149  isumshft  12201  prodeq1f  12263  prodeq2w  12267  prodeq2  12268  zproddc  12290  fprodm1s  12312  fprodp1s  12313  fprodcom2fi  12337  fprodsplitf  12343  ege2le3  12382  efgt1p2  12406  dfphi2  12942  prmdiveq  12958  pceulem  13017  sloteq  13301  setsslid  13347  ressval2  13363  ecqusaddd  13991  gfsumz  14109  ringidvalg  14204  zrhpropd  14900  metreslem  15371  comet  15490  cnmetdval  15520  dvmptfsum  15716  dvply1  15756  lgsdi  16036  lgseisenlem2  16070  lgsquadlem3  16078  uhgrvtxedgiedgb  16264  usgredg2v  16345  depindlem1  16627  redcwlpolemeq1  16965