Theorem 3eqtr4g 2215

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

Syntax hints:   → wi 4   = wceq 1335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-cleq 2150

This theorem is referenced by:  rabbidva2  2699  rabeqf  2702  csbeq1  3034  csbeq2  3055  csbeq2d  3056  csbnestgf  3083  difeq1  3218  difeq2  3219  uneq2  3255  ineq2  3302  dfrab3ss  3385  ifeq1  3508  ifeq2  3509  ifbi  3525  pweq  3546  sneq  3571  csbsng  3620  rabsn  3626  preq1  3636  preq2  3637  tpeq1  3645  tpeq2  3646  tpeq3  3647  prprc1  3667  opeq1  3741  opeq2  3742  oteq1  3750  oteq2  3751  oteq3  3752  csbunig  3780  unieq  3781  inteq  3810  iineq1  3863  iineq2  3866  dfiin2g  3882  iinrabm  3911  iinin1m  3918  iinxprg  3923  opabbid  4029  mpteq12f  4044  suceq  4362  xpeq1  4600  xpeq2  4601  csbxpg  4667  csbdmg  4780  rneq  4813  reseq1  4860  reseq2  4861  csbresg  4869  resindm  4908  resmpt  4914  resmptf  4916  imaeq1  4923  imaeq2  4924  mptcnv  4988  csbrng  5047  dmpropg  5058  rnpropg  5065  cores  5089  cores2  5098  xpcom  5132  iotaeq  5143  iotabi  5144  fntpg  5226  funimaexg  5254  fveq1  5467  fveq2  5468  fvres  5492  csbfv12g  5504  fnimapr  5528  fndmin  5574  fprg  5650  fsnunfv  5668  fsnunres  5669  fliftf  5749  isoini2  5769  riotaeqdv  5781  riotabidv  5782  riotauni  5786  riotabidva  5796  snriota  5809  oveq  5830  oveq1  5831  oveq2  5832  oprabbid  5874  mpoeq123  5880  mpoeq123dva  5882  mpoeq3dva  5885  resmpo  5919  ovres  5960  f1ocnvd  6022  ofeq  6034  ofreq  6035  f1od2  6182  ovtposg  6206  recseq  6253  tfr2a  6268  rdgeq1  6318  rdgeq2  6319  freceq1  6339  freceq2  6340  eceq1  6515  eceq2  6517  qseq1  6528  qseq2  6529  uniqs  6538  ecinxp  6555  qsinxp  6556  erovlem  6572  ixpeq1  6654  supeq1  6930  supeq2  6933  supeq3  6934  supeq123d  6935  infeq1  6955  infeq2  6958  infeq3  6959  infeq123d  6960  infisoti  6976  djueq12  6983  addpiord  7236  mulpiord  7237  00sr  7689  negeq  8068  csbnegg  8073  negsubdi  8131  mulneg1  8270  deceq1  9299  deceq2  9300  xnegeq  9731  fseq1p1m1  9996  frec2uzsucd  10300  frec2uzrdg  10308  frecuzrdgsuc  10313  frecuzrdgg  10315  frecuzrdgsuctlem  10322  seqeq1  10347  seqeq2  10348  seqeq3  10349  seqvalcd  10358  seq3f1olemp  10401  hashprg  10682  shftdm  10722  resqrexlemfp1  10909  negfi  11127  sumeq1  11252  sumeq2  11256  zsumdc  11281  isumss2  11290  fsumsplitsnun  11316  isumclim3  11320  fisumcom2  11335  isumshft  11387  prodeq1f  11449  prodeq2w  11453  prodeq2  11454  zproddc  11476  fprodm1s  11498  fprodp1s  11499  fprodcom2fi  11523  fprodsplitf  11529  ege2le3  11568  efgt1p2  11592  dfphi2  12094  prmdiveq  12110  sloteq  12195  setsslid  12240  metreslem  12780  comet  12899  cnmetdval  12929  redcwlpolemeq1  13625