Theorem 3eqtr4g 2254

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  rabbidva2  2750  rabeqf  2753  csbeq1  3087  csbeq2  3108  csbeq2d  3109  csbnestgf  3137  difeq1  3274  difeq2  3275  uneq2  3311  ineq2  3358  dfrab3ss  3441  ifeq1  3564  ifeq2  3565  ifbi  3581  pweq  3608  sneq  3633  csbsng  3683  rabsn  3689  preq1  3699  preq2  3700  tpeq1  3708  tpeq2  3709  tpeq3  3710  prprc1  3730  opeq1  3808  opeq2  3809  oteq1  3817  oteq2  3818  oteq3  3819  csbunig  3847  unieq  3848  inteq  3877  iineq1  3930  iineq2  3933  dfiin2g  3949  iinrabm  3979  iinin1m  3986  iinxprg  3991  opabbid  4098  mpteq12f  4113  suceq  4437  xpeq1  4677  xpeq2  4678  csbxpg  4744  csbdmg  4860  rneq  4893  reseq1  4940  reseq2  4941  csbresg  4949  resindm  4988  resmpt  4994  resmptf  4996  imaeq1  5004  imaeq2  5005  mptcnv  5072  csbrng  5131  dmpropg  5142  rnpropg  5149  cores  5173  cores2  5182  xpcom  5216  iotaeq  5227  iotabi  5228  fntpg  5314  funimaexg  5342  fveq1  5557  fveq2  5558  fvres  5582  csbfv12g  5596  fnimapr  5621  fndmin  5669  fprg  5745  fsnunfv  5763  fsnunres  5764  fliftf  5846  isoini2  5866  riotaeqdv  5878  riotabidv  5879  riotauni  5884  riotabidva  5894  snriota  5907  oveq  5928  oveq1  5929  oveq2  5930  oprabbid  5975  mpoeq123  5981  mpoeq123dva  5983  mpoeq3dva  5986  resmpo  6020  ovres  6063  f1ocnvd  6125  ofeqd  6137  ofeq  6138  ofreq  6139  f1od2  6293  ovtposg  6317  recseq  6364  tfr2a  6379  rdgeq1  6429  rdgeq2  6430  freceq1  6450  freceq2  6451  eceq1  6627  eceq2  6629  qseq1  6642  qseq2  6643  uniqs  6652  ecinxp  6669  qsinxp  6670  erovlem  6686  ixpeq1  6768  supeq1  7052  supeq2  7055  supeq3  7056  supeq123d  7057  infeq1  7077  infeq2  7080  infeq3  7081  infeq123d  7082  infisoti  7098  djueq12  7105  addpiord  7383  mulpiord  7384  00sr  7836  negeq  8219  csbnegg  8224  negsubdi  8282  mulneg1  8421  deceq1  9461  deceq2  9462  xnegeq  9902  fseq1p1m1  10169  frec2uzsucd  10493  frec2uzrdg  10501  frecuzrdgsuc  10506  frecuzrdgg  10508  frecuzrdgsuctlem  10515  seqeq1  10542  seqeq2  10543  seqeq3  10544  seqvalcd  10553  seq3f1olemp  10607  hashprg  10900  shftdm  10987  resqrexlemfp1  11174  negfi  11393  sumeq1  11520  sumeq2  11524  zsumdc  11549  isumss2  11558  fsumsplitsnun  11584  isumclim3  11588  fisumcom2  11603  isumshft  11655  prodeq1f  11717  prodeq2w  11721  prodeq2  11722  zproddc  11744  fprodm1s  11766  fprodp1s  11767  fprodcom2fi  11791  fprodsplitf  11797  ege2le3  11836  efgt1p2  11860  dfphi2  12388  prmdiveq  12404  pceulem  12463  sloteq  12683  setsslid  12729  ressval2  12744  ecqusaddd  13368  ringidvalg  13517  zrhpropd  14182  metreslem  14616  comet  14735  cnmetdval  14765  dvmptfsum  14961  dvply1  15001  lgsdi  15278  lgseisenlem2  15312  lgsquadlem3  15320  redcwlpolemeq1  15698