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  2852  csbeq1  3139  csbeq2d  3160  csbnestgf  3184  nineq1  3234  compleq  3243  difeq1  3246  difeq2  3247  symdifeq1  3248  symdifeq2  3249  uneq2  3412  ineq2  3451  dfrab3ss  3533  ifeq1  3666  ifeq2  3667  pweq  3725  sneq  3744  csbsng  3785  rabsn  3790  preq1  3799  preq2  3800  tpeq1  3808  tpeq2  3809  tpeq3  3810  csbunig  3899  unieq  3900  inteq  3929  iineq1  3983  iineq2  3986  dfiin2g  4000  iinrab  4028  iinin1  4037  iununi  4050  opkeq1  4059  opkeq2  4060  pw1eq  4143  cnvkeq  4215  ins2keq  4218  ins3keq  4219  imakeq1  4224  imakeq2  4225  cokeq1  4230  cokeq2  4231  p6eq  4238  sikeq  4241  imagekeq  4244  iotaeq  4347  iotabi  4348  addceq1  4383  addceq2  4384  ncfineq  4473  tfineq  4488  phieq  4570  opeq1  4578  opeq2  4579  proj1eq  4589  proj2eq  4590  opabbid  4624  xpeq1  4798  xpeq2  4799  csbxpg  4813  reseq1  4928  reseq2  4929  imaeq1  4937  imaeq2  4938  rneq  4956  csbrng  4966  csbresg  4976  resima2  5007  dmpropg  5068  cores  5084  cores2  5091  imain  5172  fveq1  5327  fveq2  5328  csbfv12g  5336  fvres  5342  fnsnfv  5373  fnimapr  5374  fvco2  5382  isoini2  5498  oveq  5529  oveq1  5530  oveq2  5531  oprabbid  5563  ovres  5602  mpteq12f  5655  mpt2eq123  5661  mpt2eq123dv  5663  mpt2eq3dva  5669  resmpt  5696  resmpt2  5697  f1od  5726  txpeq1  5779  txpeq2  5780  pprodeq1  5834  pprodeq2  5835  clos1eq1  5874  clos1eq2  5875  eceq1  5962  eceq2  5963  erth  5968  qseq1  5974  qseq2  5975  uniqs  5984  xpassen  6057  nceq  6108  tceq  6158  addcdi  6250  nchoicelem9  6297  freceq12  6311