Theorem 3eqtr4g 2289

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  rabbidva2  2787  rabeqf  2793  csbeq1  3131  csbeq2  3152  csbeq2d  3153  csbnestgf  3181  difeq1  3320  difeq2  3321  uneq2  3357  ineq2  3404  dfrab3ss  3487  ifeq1  3612  ifeq2  3613  ifbi  3630  pweq  3659  sneq  3684  csbsng  3734  rabsn  3740  preq1  3752  preq2  3753  tpeq1  3761  tpeq2  3762  tpeq3  3763  prprc1  3784  opeq1  3867  opeq2  3868  oteq1  3876  oteq2  3877  oteq3  3878  csbunig  3906  unieq  3907  inteq  3936  iineq1  3989  iineq2  3992  dfiin2g  4008  iinrabm  4038  iinin1m  4045  iinxprg  4050  opabbid  4159  mpteq12f  4174  suceq  4505  xpeq1  4745  xpeq2  4746  csbxpg  4813  csbdmg  4931  rneq  4965  reseq1  5013  reseq2  5014  csbresg  5022  resindm  5061  resmpt  5067  resmptf  5069  imaeq1  5077  imaeq2  5078  mptcnv  5146  csbrng  5205  dmpropg  5216  rnpropg  5223  cores  5247  cores2  5256  xpcom  5290  iotaeq  5302  iotabi  5303  fntpg  5393  funimaexg  5421  fveq1  5647  fveq2  5648  fvres  5672  csbfv12g  5688  fnimapr  5715  fndmin  5763  fprg  5845  fsnunfv  5863  fsnunres  5864  fliftf  5950  isoini2  5970  riotaeqdv  5982  riotabidv  5983  riotauni  5988  riotabidva  5999  snriota  6013  oveq  6034  oveq1  6035  oveq2  6036  oprabbid  6084  mpoeq123  6090  mpoeq123dva  6092  mpoeq3dva  6095  resmpo  6129  ovres  6172  f1ocnvd  6235  ofeqd  6246  ofeq  6247  ofreq  6248  f1od2  6409  ovtposg  6468  recseq  6515  tfr2a  6530  rdgeq1  6580  rdgeq2  6581  freceq1  6601  freceq2  6602  eceq1  6780  eceq2  6782  qseq1  6795  qseq2  6796  uniqs  6805  ecinxp  6822  qsinxp  6823  erovlem  6839  ixpeq1  6921  supeq1  7245  supeq2  7248  supeq3  7249  supeq123d  7250  infeq1  7270  infeq2  7273  infeq3  7274  infeq123d  7275  infisoti  7291  djueq12  7298  acneq  7477  addpiord  7596  mulpiord  7597  00sr  8049  negeq  8431  csbnegg  8436  negsubdi  8494  mulneg1  8633  deceq1  9676  deceq2  9677  xnegeq  10123  fseq1p1m1  10391  frec2uzsucd  10726  frec2uzrdg  10734  frecuzrdgsuc  10739  frecuzrdgg  10741  frecuzrdgsuctlem  10748  seqeq1  10775  seqeq2  10776  seqeq3  10777  seqvalcd  10786  seq3f1olemp  10840  hashprg  11135  s1eq  11262  s1prc  11266  s2eqd  11417  s3eqd  11418  s4eqd  11419  s5eqd  11420  s6eqd  11421  s7eqd  11422  s8eqd  11423  shftdm  11462  resqrexlemfp1  11649  negfi  11868  sumeq1  11995  sumeq2  11999  zsumdc  12025  isumss2  12034  fsumsplitsnun  12060  isumclim3  12064  fisumcom2  12079  isumshft  12131  prodeq1f  12193  prodeq2w  12197  prodeq2  12198  zproddc  12220  fprodm1s  12242  fprodp1s  12243  fprodcom2fi  12267  fprodsplitf  12273  ege2le3  12312  efgt1p2  12336  dfphi2  12872  prmdiveq  12888  pceulem  12947  sloteq  13167  setsslid  13213  ressval2  13229  ecqusaddd  13905  ringidvalg  14055  zrhpropd  14722  metreslem  15191  comet  15310  cnmetdval  15340  dvmptfsum  15536  dvply1  15576  lgsdi  15856  lgseisenlem2  15890  lgsquadlem3  15898  uhgrvtxedgiedgb  16084  usgredg2v  16165  depindlem1  16447  redcwlpolemeq1  16787