Theorem 3eqtr4g 2263

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

Syntax hints:   → wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  rabbidva2  2759  rabeqf  2762  csbeq1  3096  csbeq2  3117  csbeq2d  3118  csbnestgf  3146  difeq1  3284  difeq2  3285  uneq2  3321  ineq2  3368  dfrab3ss  3451  ifeq1  3574  ifeq2  3575  ifbi  3591  pweq  3619  sneq  3644  csbsng  3694  rabsn  3700  preq1  3710  preq2  3711  tpeq1  3719  tpeq2  3720  tpeq3  3721  prprc1  3741  opeq1  3819  opeq2  3820  oteq1  3828  oteq2  3829  oteq3  3830  csbunig  3858  unieq  3859  inteq  3888  iineq1  3941  iineq2  3944  dfiin2g  3960  iinrabm  3990  iinin1m  3997  iinxprg  4002  opabbid  4110  mpteq12f  4125  suceq  4450  xpeq1  4690  xpeq2  4691  csbxpg  4757  csbdmg  4873  rneq  4906  reseq1  4954  reseq2  4955  csbresg  4963  resindm  5002  resmpt  5008  resmptf  5010  imaeq1  5018  imaeq2  5019  mptcnv  5086  csbrng  5145  dmpropg  5156  rnpropg  5163  cores  5187  cores2  5196  xpcom  5230  iotaeq  5241  iotabi  5242  fntpg  5331  funimaexg  5359  fveq1  5577  fveq2  5578  fvres  5602  csbfv12g  5616  fnimapr  5641  fndmin  5689  fprg  5769  fsnunfv  5787  fsnunres  5788  fliftf  5870  isoini2  5890  riotaeqdv  5902  riotabidv  5903  riotauni  5908  riotabidva  5918  snriota  5931  oveq  5952  oveq1  5953  oveq2  5954  oprabbid  6000  mpoeq123  6006  mpoeq123dva  6008  mpoeq3dva  6011  resmpo  6045  ovres  6088  f1ocnvd  6150  ofeqd  6162  ofeq  6163  ofreq  6164  f1od2  6323  ovtposg  6347  recseq  6394  tfr2a  6409  rdgeq1  6459  rdgeq2  6460  freceq1  6480  freceq2  6481  eceq1  6657  eceq2  6659  qseq1  6672  qseq2  6673  uniqs  6682  ecinxp  6699  qsinxp  6700  erovlem  6716  ixpeq1  6798  supeq1  7090  supeq2  7093  supeq3  7094  supeq123d  7095  infeq1  7115  infeq2  7118  infeq3  7119  infeq123d  7120  infisoti  7136  djueq12  7143  acneq  7316  addpiord  7431  mulpiord  7432  00sr  7884  negeq  8267  csbnegg  8272  negsubdi  8330  mulneg1  8469  deceq1  9510  deceq2  9511  xnegeq  9951  fseq1p1m1  10218  frec2uzsucd  10548  frec2uzrdg  10556  frecuzrdgsuc  10561  frecuzrdgg  10563  frecuzrdgsuctlem  10570  seqeq1  10597  seqeq2  10598  seqeq3  10599  seqvalcd  10608  seq3f1olemp  10662  hashprg  10955  s1eq  11076  s1prc  11080  shftdm  11166  resqrexlemfp1  11353  negfi  11572  sumeq1  11699  sumeq2  11703  zsumdc  11728  isumss2  11737  fsumsplitsnun  11763  isumclim3  11767  fisumcom2  11782  isumshft  11834  prodeq1f  11896  prodeq2w  11900  prodeq2  11901  zproddc  11923  fprodm1s  11945  fprodp1s  11946  fprodcom2fi  11970  fprodsplitf  11976  ege2le3  12015  efgt1p2  12039  dfphi2  12575  prmdiveq  12591  pceulem  12650  sloteq  12870  setsslid  12916  ressval2  12931  ecqusaddd  13607  ringidvalg  13756  zrhpropd  14421  metreslem  14885  comet  15004  cnmetdval  15034  dvmptfsum  15230  dvply1  15270  lgsdi  15547  lgseisenlem2  15581  lgsquadlem3  15589  redcwlpolemeq1  16030