Theorem 3eqtr4g 2287

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  rabbidva2  2786  rabeqf  2789  csbeq1  3127  csbeq2  3148  csbeq2d  3149  csbnestgf  3177  difeq1  3315  difeq2  3316  uneq2  3352  ineq2  3399  dfrab3ss  3482  ifeq1  3605  ifeq2  3606  ifbi  3623  pweq  3652  sneq  3677  csbsng  3727  rabsn  3733  preq1  3743  preq2  3744  tpeq1  3752  tpeq2  3753  tpeq3  3754  prprc1  3775  opeq1  3857  opeq2  3858  oteq1  3866  oteq2  3867  oteq3  3868  csbunig  3896  unieq  3897  inteq  3926  iineq1  3979  iineq2  3982  dfiin2g  3998  iinrabm  4028  iinin1m  4035  iinxprg  4040  opabbid  4149  mpteq12f  4164  suceq  4493  xpeq1  4733  xpeq2  4734  csbxpg  4800  csbdmg  4917  rneq  4951  reseq1  4999  reseq2  5000  csbresg  5008  resindm  5047  resmpt  5053  resmptf  5055  imaeq1  5063  imaeq2  5064  mptcnv  5131  csbrng  5190  dmpropg  5201  rnpropg  5208  cores  5232  cores2  5241  xpcom  5275  iotaeq  5287  iotabi  5288  fntpg  5377  funimaexg  5405  fveq1  5628  fveq2  5629  fvres  5653  csbfv12g  5669  fnimapr  5696  fndmin  5744  fprg  5826  fsnunfv  5844  fsnunres  5845  fliftf  5929  isoini2  5949  riotaeqdv  5961  riotabidv  5962  riotauni  5967  riotabidva  5978  snriota  5992  oveq  6013  oveq1  6014  oveq2  6015  oprabbid  6063  mpoeq123  6069  mpoeq123dva  6071  mpoeq3dva  6074  resmpo  6108  ovres  6151  f1ocnvd  6214  ofeqd  6226  ofeq  6227  ofreq  6228  f1od2  6387  ovtposg  6411  recseq  6458  tfr2a  6473  rdgeq1  6523  rdgeq2  6524  freceq1  6544  freceq2  6545  eceq1  6723  eceq2  6725  qseq1  6738  qseq2  6739  uniqs  6748  ecinxp  6765  qsinxp  6766  erovlem  6782  ixpeq1  6864  supeq1  7164  supeq2  7167  supeq3  7168  supeq123d  7169  infeq1  7189  infeq2  7192  infeq3  7193  infeq123d  7194  infisoti  7210  djueq12  7217  acneq  7395  addpiord  7514  mulpiord  7515  00sr  7967  negeq  8350  csbnegg  8355  negsubdi  8413  mulneg1  8552  deceq1  9593  deceq2  9594  xnegeq  10035  fseq1p1m1  10302  frec2uzsucd  10635  frec2uzrdg  10643  frecuzrdgsuc  10648  frecuzrdgg  10650  frecuzrdgsuctlem  10657  seqeq1  10684  seqeq2  10685  seqeq3  10686  seqvalcd  10695  seq3f1olemp  10749  hashprg  11043  s1eq  11167  s1prc  11171  s2eqd  11318  s3eqd  11319  s4eqd  11320  s5eqd  11321  s6eqd  11322  s7eqd  11323  s8eqd  11324  shftdm  11349  resqrexlemfp1  11536  negfi  11755  sumeq1  11882  sumeq2  11886  zsumdc  11911  isumss2  11920  fsumsplitsnun  11946  isumclim3  11950  fisumcom2  11965  isumshft  12017  prodeq1f  12079  prodeq2w  12083  prodeq2  12084  zproddc  12106  fprodm1s  12128  fprodp1s  12129  fprodcom2fi  12153  fprodsplitf  12159  ege2le3  12198  efgt1p2  12222  dfphi2  12758  prmdiveq  12774  pceulem  12833  sloteq  13053  setsslid  13099  ressval2  13115  ecqusaddd  13791  ringidvalg  13940  zrhpropd  14606  metreslem  15070  comet  15189  cnmetdval  15219  dvmptfsum  15415  dvply1  15455  lgsdi  15732  lgseisenlem2  15766  lgsquadlem3  15774  uhgrvtxedgiedgb  15957  usgredg2v  16038  redcwlpolemeq1  16510