Theorem 3eqtr4g 2410

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3eqtr4g.1	⊢ (φ → A = B)
3eqtr4g.2	⊢ C = A
3eqtr4g.3	⊢ D = B

Assertion

Ref	Expression
3eqtr4g	⊢ (φ → C = D)

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 ⊢ C = A
2		3eqtr4g.1	. . 3 ⊢ (φ → A = B)
3	1, 2	syl5eq 2397	. 2 ⊢ (φ → C = B)
4		3eqtr4g.3	. 2 ⊢ D = B
5	3, 4	syl6eqr 2403	1 ⊢ (φ → C = D)

Syntax hints:   → wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  rabeqf  2853  csbeq1  3140  csbeq2d  3161  csbnestgf  3185  nineq1  3235  compleq  3244  difeq1  3247  difeq2  3248  symdifeq1  3249  symdifeq2  3250  uneq2  3413  ineq2  3452  dfrab3ss  3534  ifeq1  3667  ifeq2  3668  pweq  3726  sneq  3745  csbsng  3786  rabsn  3791  preq1  3800  preq2  3801  tpeq1  3809  tpeq2  3810  tpeq3  3811  csbunig  3900  unieq  3901  inteq  3930  iineq1  3984  iineq2  3987  dfiin2g  4001  iinrab  4029  iinin1  4038  iununi  4051  opkeq1  4060  opkeq2  4061  pw1eq  4144  cnvkeq  4216  ins2keq  4219  ins3keq  4220  imakeq1  4225  imakeq2  4226  cokeq1  4231  cokeq2  4232  p6eq  4239  sikeq  4242  imagekeq  4245  iotaeq  4348  iotabi  4349  addceq1  4384  addceq2  4385  ncfineq  4474  tfineq  4489  phieq  4571  opeq1  4579  opeq2  4580  proj1eq  4590  proj2eq  4591  opabbid  4625  xpeq1  4799  xpeq2  4800  csbxpg  4814  reseq1  4929  reseq2  4930  imaeq1  4938  imaeq2  4939  rneq  4957  csbrng  4967  csbresg  4977  resima2  5008  dmpropg  5069  cores  5085  cores2  5092  imain  5173  fveq1  5328  fveq2  5329  csbfv12g  5337  fvres  5343  fnsnfv  5374  fnimapr  5375  fvco2  5383  isoini2  5499  oveq  5530  oveq1  5531  oveq2  5532  oprabbid  5564  ovres  5603  mpteq12f  5656  mpt2eq123  5662  mpt2eq123dv  5664  mpt2eq3dva  5670  resmpt  5697  resmpt2  5698  f1od  5727  txpeq1  5780  txpeq2  5781  pprodeq1  5835  pprodeq2  5836  clos1eq1  5875  clos1eq2  5876  eceq1  5963  eceq2  5964  erth  5969  qseq1  5975  qseq2  5976  uniqs  5985  xpassen  6058  nceq  6109  tceq  6159  addcdi  6251  nchoicelem9  6298  freceq12  6312