Theorem 3eqtr4g 2197

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

Syntax hints:   → wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  rabbidva2  2673  rabeqf  2676  csbeq1  3006  csbeq2  3026  csbeq2d  3027  csbnestgf  3052  difeq1  3187  difeq2  3188  uneq2  3224  ineq2  3271  dfrab3ss  3354  ifeq1  3477  ifeq2  3478  ifbi  3492  pweq  3513  sneq  3538  csbsng  3584  rabsn  3590  preq1  3600  preq2  3601  tpeq1  3609  tpeq2  3610  tpeq3  3611  prprc1  3631  opeq1  3705  opeq2  3706  oteq1  3714  oteq2  3715  oteq3  3716  csbunig  3744  unieq  3745  inteq  3774  iineq1  3827  iineq2  3830  dfiin2g  3846  iinrabm  3875  iinin1m  3882  iinxprg  3887  opabbid  3993  mpteq12f  4008  suceq  4324  xpeq1  4553  xpeq2  4554  csbxpg  4620  csbdmg  4733  rneq  4766  reseq1  4813  reseq2  4814  csbresg  4822  resindm  4861  resmpt  4867  resmptf  4869  imaeq1  4876  imaeq2  4877  mptcnv  4941  csbrng  5000  dmpropg  5011  rnpropg  5018  cores  5042  cores2  5051  xpcom  5085  iotaeq  5096  iotabi  5097  fntpg  5179  funimaexg  5207  fveq1  5420  fveq2  5421  fvres  5445  csbfv12g  5457  fnimapr  5481  fndmin  5527  fprg  5603  fsnunfv  5621  fsnunres  5622  fliftf  5700  isoini2  5720  riotaeqdv  5731  riotabidv  5732  riotauni  5736  riotabidva  5746  snriota  5759  oveq  5780  oveq1  5781  oveq2  5782  oprabbid  5824  mpoeq123  5830  mpoeq123dva  5832  mpoeq3dva  5835  resmpo  5869  ovres  5910  f1ocnvd  5972  ofeq  5984  ofreq  5985  f1od2  6132  ovtposg  6156  recseq  6203  tfr2a  6218  rdgeq1  6268  rdgeq2  6269  freceq1  6289  freceq2  6290  eceq1  6464  eceq2  6466  qseq1  6477  qseq2  6478  uniqs  6487  ecinxp  6504  qsinxp  6505  erovlem  6521  ixpeq1  6603  supeq1  6873  supeq2  6876  supeq3  6877  supeq123d  6878  infeq1  6898  infeq2  6901  infeq3  6902  infeq123d  6903  infisoti  6919  djueq12  6924  addpiord  7124  mulpiord  7125  00sr  7577  negeq  7955  csbnegg  7960  negsubdi  8018  mulneg1  8157  deceq1  9186  deceq2  9187  xnegeq  9610  fseq1p1m1  9874  frec2uzsucd  10174  frec2uzrdg  10182  frecuzrdgsuc  10187  frecuzrdgg  10189  frecuzrdgsuctlem  10196  seqeq1  10221  seqeq2  10222  seqeq3  10223  seqvalcd  10232  seq3f1olemp  10275  hashprg  10554  shftdm  10594  resqrexlemfp1  10781  negfi  10999  sumeq1  11124  sumeq2  11128  zsumdc  11153  isumss2  11162  fsumsplitsnun  11188  isumclim3  11192  fisumcom2  11207  isumshft  11259  prodeq1f  11321  prodeq2w  11325  prodeq2  11326  ege2le3  11377  efgt1p2  11401  dfphi2  11896  sloteq  11964  setsslid  12009  metreslem  12549  comet  12668  cnmetdval  12698