Theorem 3eqtr4g 2265

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 2252	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2258	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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  rabbidva2  2763  rabeqf  2766  csbeq1  3104  csbeq2  3125  csbeq2d  3126  csbnestgf  3154  difeq1  3292  difeq2  3293  uneq2  3329  ineq2  3376  dfrab3ss  3459  ifeq1  3582  ifeq2  3583  ifbi  3600  pweq  3629  sneq  3654  csbsng  3704  rabsn  3710  preq1  3720  preq2  3721  tpeq1  3729  tpeq2  3730  tpeq3  3731  prprc1  3751  opeq1  3833  opeq2  3834  oteq1  3842  oteq2  3843  oteq3  3844  csbunig  3872  unieq  3873  inteq  3902  iineq1  3955  iineq2  3958  dfiin2g  3974  iinrabm  4004  iinin1m  4011  iinxprg  4016  opabbid  4125  mpteq12f  4140  suceq  4467  xpeq1  4707  xpeq2  4708  csbxpg  4774  csbdmg  4891  rneq  4924  reseq1  4972  reseq2  4973  csbresg  4981  resindm  5020  resmpt  5026  resmptf  5028  imaeq1  5036  imaeq2  5037  mptcnv  5104  csbrng  5163  dmpropg  5174  rnpropg  5181  cores  5205  cores2  5214  xpcom  5248  iotaeq  5259  iotabi  5260  fntpg  5349  funimaexg  5377  fveq1  5598  fveq2  5599  fvres  5623  csbfv12g  5637  fnimapr  5662  fndmin  5710  fprg  5790  fsnunfv  5808  fsnunres  5809  fliftf  5891  isoini2  5911  riotaeqdv  5923  riotabidv  5924  riotauni  5929  riotabidva  5939  snriota  5952  oveq  5973  oveq1  5974  oveq2  5975  oprabbid  6021  mpoeq123  6027  mpoeq123dva  6029  mpoeq3dva  6032  resmpo  6066  ovres  6109  f1ocnvd  6171  ofeqd  6183  ofeq  6184  ofreq  6185  f1od2  6344  ovtposg  6368  recseq  6415  tfr2a  6430  rdgeq1  6480  rdgeq2  6481  freceq1  6501  freceq2  6502  eceq1  6678  eceq2  6680  qseq1  6693  qseq2  6694  uniqs  6703  ecinxp  6720  qsinxp  6721  erovlem  6737  ixpeq1  6819  supeq1  7114  supeq2  7117  supeq3  7118  supeq123d  7119  infeq1  7139  infeq2  7142  infeq3  7143  infeq123d  7144  infisoti  7160  djueq12  7167  acneq  7345  addpiord  7464  mulpiord  7465  00sr  7917  negeq  8300  csbnegg  8305  negsubdi  8363  mulneg1  8502  deceq1  9543  deceq2  9544  xnegeq  9984  fseq1p1m1  10251  frec2uzsucd  10583  frec2uzrdg  10591  frecuzrdgsuc  10596  frecuzrdgg  10598  frecuzrdgsuctlem  10605  seqeq1  10632  seqeq2  10633  seqeq3  10634  seqvalcd  10643  seq3f1olemp  10697  hashprg  10990  s1eq  11111  s1prc  11115  shftdm  11248  resqrexlemfp1  11435  negfi  11654  sumeq1  11781  sumeq2  11785  zsumdc  11810  isumss2  11819  fsumsplitsnun  11845  isumclim3  11849  fisumcom2  11864  isumshft  11916  prodeq1f  11978  prodeq2w  11982  prodeq2  11983  zproddc  12005  fprodm1s  12027  fprodp1s  12028  fprodcom2fi  12052  fprodsplitf  12058  ege2le3  12097  efgt1p2  12121  dfphi2  12657  prmdiveq  12673  pceulem  12732  sloteq  12952  setsslid  12998  ressval2  13013  ecqusaddd  13689  ringidvalg  13838  zrhpropd  14503  metreslem  14967  comet  15086  cnmetdval  15116  dvmptfsum  15312  dvply1  15352  lgsdi  15629  lgseisenlem2  15663  lgsquadlem3  15671  uhgrvtxedgiedgb  15847  redcwlpolemeq1  16195