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  2784  rabeqf  2790  csbeq1  3128  csbeq2  3149  csbeq2d  3150  csbnestgf  3178  difeq1  3316  difeq2  3317  uneq2  3353  ineq2  3400  dfrab3ss  3483  ifeq1  3606  ifeq2  3607  ifbi  3624  pweq  3653  sneq  3678  csbsng  3728  rabsn  3734  preq1  3746  preq2  3747  tpeq1  3755  tpeq2  3756  tpeq3  3757  prprc1  3778  opeq1  3860  opeq2  3861  oteq1  3869  oteq2  3870  oteq3  3871  csbunig  3899  unieq  3900  inteq  3929  iineq1  3982  iineq2  3985  dfiin2g  4001  iinrabm  4031  iinin1m  4038  iinxprg  4043  opabbid  4152  mpteq12f  4167  suceq  4497  xpeq1  4737  xpeq2  4738  csbxpg  4805  csbdmg  4923  rneq  4957  reseq1  5005  reseq2  5006  csbresg  5014  resindm  5053  resmpt  5059  resmptf  5061  imaeq1  5069  imaeq2  5070  mptcnv  5137  csbrng  5196  dmpropg  5207  rnpropg  5214  cores  5238  cores2  5247  xpcom  5281  iotaeq  5293  iotabi  5294  fntpg  5383  funimaexg  5411  fveq1  5634  fveq2  5635  fvres  5659  csbfv12g  5675  fnimapr  5702  fndmin  5750  fprg  5832  fsnunfv  5850  fsnunres  5851  fliftf  5935  isoini2  5955  riotaeqdv  5967  riotabidv  5968  riotauni  5973  riotabidva  5984  snriota  5998  oveq  6019  oveq1  6020  oveq2  6021  oprabbid  6069  mpoeq123  6075  mpoeq123dva  6077  mpoeq3dva  6080  resmpo  6114  ovres  6157  f1ocnvd  6220  ofeqd  6232  ofeq  6233  ofreq  6234  f1od2  6395  ovtposg  6420  recseq  6467  tfr2a  6482  rdgeq1  6532  rdgeq2  6533  freceq1  6553  freceq2  6554  eceq1  6732  eceq2  6734  qseq1  6747  qseq2  6748  uniqs  6757  ecinxp  6774  qsinxp  6775  erovlem  6791  ixpeq1  6873  supeq1  7176  supeq2  7179  supeq3  7180  supeq123d  7181  infeq1  7201  infeq2  7204  infeq3  7205  infeq123d  7206  infisoti  7222  djueq12  7229  acneq  7407  addpiord  7526  mulpiord  7527  00sr  7979  negeq  8362  csbnegg  8367  negsubdi  8425  mulneg1  8564  deceq1  9605  deceq2  9606  xnegeq  10052  fseq1p1m1  10319  frec2uzsucd  10653  frec2uzrdg  10661  frecuzrdgsuc  10666  frecuzrdgg  10668  frecuzrdgsuctlem  10675  seqeq1  10702  seqeq2  10703  seqeq3  10704  seqvalcd  10713  seq3f1olemp  10767  hashprg  11062  s1eq  11186  s1prc  11190  s2eqd  11341  s3eqd  11342  s4eqd  11343  s5eqd  11344  s6eqd  11345  s7eqd  11346  s8eqd  11347  shftdm  11373  resqrexlemfp1  11560  negfi  11779  sumeq1  11906  sumeq2  11910  zsumdc  11935  isumss2  11944  fsumsplitsnun  11970  isumclim3  11974  fisumcom2  11989  isumshft  12041  prodeq1f  12103  prodeq2w  12107  prodeq2  12108  zproddc  12130  fprodm1s  12152  fprodp1s  12153  fprodcom2fi  12177  fprodsplitf  12183  ege2le3  12222  efgt1p2  12246  dfphi2  12782  prmdiveq  12798  pceulem  12857  sloteq  13077  setsslid  13123  ressval2  13139  ecqusaddd  13815  ringidvalg  13964  zrhpropd  14630  metreslem  15094  comet  15213  cnmetdval  15243  dvmptfsum  15439  dvply1  15479  lgsdi  15756  lgseisenlem2  15790  lgsquadlem3  15798  uhgrvtxedgiedgb  15982  usgredg2v  16063  redcwlpolemeq1  16594