Theorem 3eqtr4g 2296

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

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  rabbidva2  2805  rabeqf  2811  csbeq1  3150  csbeq2  3171  csbeq2d  3172  csbnestgf  3200  difeq1  3340  difeq2  3341  uneq2  3377  ineq2  3426  dfrab3ss  3511  ifeq1  3640  ifeq2  3641  ifbi  3658  pweq  3688  sneq  3716  csbsng  3766  rabsn  3772  preq1  3784  preq2  3785  tpeq1  3793  tpeq2  3794  tpeq3  3795  prprc1  3816  opeq1  3899  opeq2  3900  oteq1  3908  oteq2  3909  oteq3  3910  csbunig  3938  unieq  3939  inteq  3968  iineq1  4021  iineq2  4024  dfiin2g  4040  iinrabm  4070  iinin1m  4077  iinxprg  4082  opabbid  4191  mpteq12f  4206  suceq  4542  xpeq1  4783  xpeq2  4784  csbxpg  4851  csbdmg  4970  rneq  5004  reseq1  5052  reseq2  5053  csbresg  5061  resindm  5100  resmpt  5106  resmptf  5108  imaeq1  5116  imaeq2  5117  mptcnv  5185  csbrng  5244  dmpropg  5255  rnpropg  5262  cores  5286  cores2  5295  xpcom  5329  iotaeq  5341  iotabi  5342  fntpg  5432  funimaexg  5460  fveq1  5689  fveq2  5690  fvres  5714  csbfv12g  5730  fnimapr  5757  fndmin  5807  fprg  5889  fsnunfv  5907  fsnunres  5908  fliftf  5995  isoini2  6015  riotaeqdv  6029  riotabidv  6030  riotauni  6035  riotabidva  6046  snriota  6060  oveq  6081  oveq1  6082  oveq2  6083  oprabbid  6131  mpoeq123  6137  mpoeq123dva  6139  mpoeq3dva  6142  resmpo  6176  ovres  6219  f1ocnvd  6282  ofeqd  6294  ofeq  6295  ofreq  6296  f1od2  6461  ovtposg  6520  recseq  6567  tfr2a  6582  rdgeq1  6632  rdgeq2  6633  freceq1  6653  freceq2  6654  eceq1  6832  eceq2  6834  qseq1  6847  qseq2  6848  uniqs  6857  ecinxp  6874  qsinxp  6875  erovlem  6891  ixpeq1  6981  supeq1  7316  supeq2  7319  supeq3  7320  supeq123d  7321  infeq1  7341  infeq2  7344  infeq3  7345  infeq123d  7346  infisoti  7362  djueq12  7369  acneq  7548  addpiord  7673  mulpiord  7674  00sr  8126  negeq  8509  csbnegg  8514  negsubdi  8572  mulneg1  8712  deceq1  9760  deceq2  9761  xnegeq  10208  fseq1p1m1  10479  frec2uzsucd  10816  frec2uzrdg  10824  frecuzrdgsuc  10829  frecuzrdgg  10831  frecuzrdgsuctlem  10838  seqeq1  10865  seqeq2  10866  seqeq3  10867  seqvalcd  10876  seq3f1olemp  10930  hashprg  11227  s1eq  11365  s1prc  11369  s2eqd  11520  s3eqd  11521  s4eqd  11522  s5eqd  11523  s6eqd  11524  s7eqd  11525  s8eqd  11526  shftdm  11565  resqrexlemfp1  11753  negfi  11972  sumeq1  12099  sumeq2  12103  zsumdc  12129  isumss2  12138  fsumsplitsnun  12164  isumclim3  12168  fisumcom2  12183  isumshft  12235  prodeq1f  12297  prodeq2w  12301  prodeq2  12302  zproddc  12324  fprodm1s  12346  fprodp1s  12347  fprodcom2fi  12371  fprodsplitf  12377  ege2le3  12416  efgt1p2  12440  dfphi2  12976  prmdiveq  12992  pceulem  13051  sloteq  13335  setsslid  13381  ressval2  13397  ecqusaddd  14018  gsumzfi  14135  gsumsubmclfi  14140  ringidvalg  14239  zrhpropd  14933  metreslem  15404  comet  15523  cnmetdval  15553  dvmptfsum  15749  dvply1  15789  lgsdi  16070  lgseisenlem2  16104  lgsquadlem3  16112  uhgrvtxedgiedgb  16298  usgredg2v  16379  depindlem1  16661  redcwlpolemeq1  17009