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  3275  difeq2  3276  uneq2  3312  ineq2  3359  dfrab3ss  3442  ifeq1  3565  ifeq2  3566  ifbi  3582  pweq  3609  sneq  3634  csbsng  3684  rabsn  3690  preq1  3700  preq2  3701  tpeq1  3709  tpeq2  3710  tpeq3  3711  prprc1  3731  opeq1  3809  opeq2  3810  oteq1  3818  oteq2  3819  oteq3  3820  csbunig  3848  unieq  3849  inteq  3878  iineq1  3931  iineq2  3934  dfiin2g  3950  iinrabm  3980  iinin1m  3987  iinxprg  3992  opabbid  4099  mpteq12f  4114  suceq  4438  xpeq1  4678  xpeq2  4679  csbxpg  4745  csbdmg  4861  rneq  4894  reseq1  4941  reseq2  4942  csbresg  4950  resindm  4989  resmpt  4995  resmptf  4997  imaeq1  5005  imaeq2  5006  mptcnv  5073  csbrng  5132  dmpropg  5143  rnpropg  5150  cores  5174  cores2  5183  xpcom  5217  iotaeq  5228  iotabi  5229  fntpg  5315  funimaexg  5343  fveq1  5560  fveq2  5561  fvres  5585  csbfv12g  5599  fnimapr  5624  fndmin  5672  fprg  5748  fsnunfv  5766  fsnunres  5767  fliftf  5849  isoini2  5869  riotaeqdv  5881  riotabidv  5882  riotauni  5887  riotabidva  5897  snriota  5910  oveq  5931  oveq1  5932  oveq2  5933  oprabbid  5979  mpoeq123  5985  mpoeq123dva  5987  mpoeq3dva  5990  resmpo  6024  ovres  6067  f1ocnvd  6129  ofeqd  6141  ofeq  6142  ofreq  6143  f1od2  6302  ovtposg  6326  recseq  6373  tfr2a  6388  rdgeq1  6438  rdgeq2  6439  freceq1  6459  freceq2  6460  eceq1  6636  eceq2  6638  qseq1  6651  qseq2  6652  uniqs  6661  ecinxp  6678  qsinxp  6679  erovlem  6695  ixpeq1  6777  supeq1  7061  supeq2  7064  supeq3  7065  supeq123d  7066  infeq1  7086  infeq2  7089  infeq3  7090  infeq123d  7091  infisoti  7107  djueq12  7114  acneq  7285  addpiord  7400  mulpiord  7401  00sr  7853  negeq  8236  csbnegg  8241  negsubdi  8299  mulneg1  8438  deceq1  9478  deceq2  9479  xnegeq  9919  fseq1p1m1  10186  frec2uzsucd  10510  frec2uzrdg  10518  frecuzrdgsuc  10523  frecuzrdgg  10525  frecuzrdgsuctlem  10532  seqeq1  10559  seqeq2  10560  seqeq3  10561  seqvalcd  10570  seq3f1olemp  10624  hashprg  10917  shftdm  11004  resqrexlemfp1  11191  negfi  11410  sumeq1  11537  sumeq2  11541  zsumdc  11566  isumss2  11575  fsumsplitsnun  11601  isumclim3  11605  fisumcom2  11620  isumshft  11672  prodeq1f  11734  prodeq2w  11738  prodeq2  11739  zproddc  11761  fprodm1s  11783  fprodp1s  11784  fprodcom2fi  11808  fprodsplitf  11814  ege2le3  11853  efgt1p2  11877  dfphi2  12413  prmdiveq  12429  pceulem  12488  sloteq  12708  setsslid  12754  ressval2  12769  ecqusaddd  13444  ringidvalg  13593  zrhpropd  14258  metreslem  14700  comet  14819  cnmetdval  14849  dvmptfsum  15045  dvply1  15085  lgsdi  15362  lgseisenlem2  15396  lgsquadlem3  15404  redcwlpolemeq1  15785