Theorem 3eqtr4g 2263

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

Syntax hints:   → wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  rabbidva2  2759  rabeqf  2762  csbeq1  3096  csbeq2  3117  csbeq2d  3118  csbnestgf  3146  difeq1  3284  difeq2  3285  uneq2  3321  ineq2  3368  dfrab3ss  3451  ifeq1  3574  ifeq2  3575  ifbi  3591  pweq  3619  sneq  3644  csbsng  3694  rabsn  3700  preq1  3710  preq2  3711  tpeq1  3719  tpeq2  3720  tpeq3  3721  prprc1  3741  opeq1  3819  opeq2  3820  oteq1  3828  oteq2  3829  oteq3  3830  csbunig  3858  unieq  3859  inteq  3888  iineq1  3941  iineq2  3944  dfiin2g  3960  iinrabm  3990  iinin1m  3997  iinxprg  4002  opabbid  4109  mpteq12f  4124  suceq  4449  xpeq1  4689  xpeq2  4690  csbxpg  4756  csbdmg  4872  rneq  4905  reseq1  4953  reseq2  4954  csbresg  4962  resindm  5001  resmpt  5007  resmptf  5009  imaeq1  5017  imaeq2  5018  mptcnv  5085  csbrng  5144  dmpropg  5155  rnpropg  5162  cores  5186  cores2  5195  xpcom  5229  iotaeq  5240  iotabi  5241  fntpg  5330  funimaexg  5358  fveq1  5575  fveq2  5576  fvres  5600  csbfv12g  5614  fnimapr  5639  fndmin  5687  fprg  5767  fsnunfv  5785  fsnunres  5786  fliftf  5868  isoini2  5888  riotaeqdv  5900  riotabidv  5901  riotauni  5906  riotabidva  5916  snriota  5929  oveq  5950  oveq1  5951  oveq2  5952  oprabbid  5998  mpoeq123  6004  mpoeq123dva  6006  mpoeq3dva  6009  resmpo  6043  ovres  6086  f1ocnvd  6148  ofeqd  6160  ofeq  6161  ofreq  6162  f1od2  6321  ovtposg  6345  recseq  6392  tfr2a  6407  rdgeq1  6457  rdgeq2  6458  freceq1  6478  freceq2  6479  eceq1  6655  eceq2  6657  qseq1  6670  qseq2  6671  uniqs  6680  ecinxp  6697  qsinxp  6698  erovlem  6714  ixpeq1  6796  supeq1  7088  supeq2  7091  supeq3  7092  supeq123d  7093  infeq1  7113  infeq2  7116  infeq3  7117  infeq123d  7118  infisoti  7134  djueq12  7141  acneq  7314  addpiord  7429  mulpiord  7430  00sr  7882  negeq  8265  csbnegg  8270  negsubdi  8328  mulneg1  8467  deceq1  9508  deceq2  9509  xnegeq  9949  fseq1p1m1  10216  frec2uzsucd  10546  frec2uzrdg  10554  frecuzrdgsuc  10559  frecuzrdgg  10561  frecuzrdgsuctlem  10568  seqeq1  10595  seqeq2  10596  seqeq3  10597  seqvalcd  10606  seq3f1olemp  10660  hashprg  10953  s1eq  11073  s1prc  11077  shftdm  11133  resqrexlemfp1  11320  negfi  11539  sumeq1  11666  sumeq2  11670  zsumdc  11695  isumss2  11704  fsumsplitsnun  11730  isumclim3  11734  fisumcom2  11749  isumshft  11801  prodeq1f  11863  prodeq2w  11867  prodeq2  11868  zproddc  11890  fprodm1s  11912  fprodp1s  11913  fprodcom2fi  11937  fprodsplitf  11943  ege2le3  11982  efgt1p2  12006  dfphi2  12542  prmdiveq  12558  pceulem  12617  sloteq  12837  setsslid  12883  ressval2  12898  ecqusaddd  13574  ringidvalg  13723  zrhpropd  14388  metreslem  14852  comet  14971  cnmetdval  15001  dvmptfsum  15197  dvply1  15237  lgsdi  15514  lgseisenlem2  15548  lgsquadlem3  15556  redcwlpolemeq1  15993