Theorem 3eqtr4g 2251

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  rabbidva2  2747  rabeqf  2750  csbeq1  3083  csbeq2  3104  csbeq2d  3105  csbnestgf  3133  difeq1  3270  difeq2  3271  uneq2  3307  ineq2  3354  dfrab3ss  3437  ifeq1  3560  ifeq2  3561  ifbi  3577  pweq  3604  sneq  3629  csbsng  3679  rabsn  3685  preq1  3695  preq2  3696  tpeq1  3704  tpeq2  3705  tpeq3  3706  prprc1  3726  opeq1  3804  opeq2  3805  oteq1  3813  oteq2  3814  oteq3  3815  csbunig  3843  unieq  3844  inteq  3873  iineq1  3926  iineq2  3929  dfiin2g  3945  iinrabm  3975  iinin1m  3982  iinxprg  3987  opabbid  4094  mpteq12f  4109  suceq  4433  xpeq1  4673  xpeq2  4674  csbxpg  4740  csbdmg  4856  rneq  4889  reseq1  4936  reseq2  4937  csbresg  4945  resindm  4984  resmpt  4990  resmptf  4992  imaeq1  5000  imaeq2  5001  mptcnv  5068  csbrng  5127  dmpropg  5138  rnpropg  5145  cores  5169  cores2  5178  xpcom  5212  iotaeq  5223  iotabi  5224  fntpg  5310  funimaexg  5338  fveq1  5553  fveq2  5554  fvres  5578  csbfv12g  5592  fnimapr  5617  fndmin  5665  fprg  5741  fsnunfv  5759  fsnunres  5760  fliftf  5842  isoini2  5862  riotaeqdv  5874  riotabidv  5875  riotauni  5880  riotabidva  5890  snriota  5903  oveq  5924  oveq1  5925  oveq2  5926  oprabbid  5971  mpoeq123  5977  mpoeq123dva  5979  mpoeq3dva  5982  resmpo  6016  ovres  6058  f1ocnvd  6120  ofeqd  6132  ofeq  6133  ofreq  6134  f1od2  6288  ovtposg  6312  recseq  6359  tfr2a  6374  rdgeq1  6424  rdgeq2  6425  freceq1  6445  freceq2  6446  eceq1  6622  eceq2  6624  qseq1  6637  qseq2  6638  uniqs  6647  ecinxp  6664  qsinxp  6665  erovlem  6681  ixpeq1  6763  supeq1  7045  supeq2  7048  supeq3  7049  supeq123d  7050  infeq1  7070  infeq2  7073  infeq3  7074  infeq123d  7075  infisoti  7091  djueq12  7098  addpiord  7376  mulpiord  7377  00sr  7829  negeq  8212  csbnegg  8217  negsubdi  8275  mulneg1  8414  deceq1  9452  deceq2  9453  xnegeq  9893  fseq1p1m1  10160  frec2uzsucd  10472  frec2uzrdg  10480  frecuzrdgsuc  10485  frecuzrdgg  10487  frecuzrdgsuctlem  10494  seqeq1  10521  seqeq2  10522  seqeq3  10523  seqvalcd  10532  seq3f1olemp  10586  hashprg  10879  shftdm  10966  resqrexlemfp1  11153  negfi  11371  sumeq1  11498  sumeq2  11502  zsumdc  11527  isumss2  11536  fsumsplitsnun  11562  isumclim3  11566  fisumcom2  11581  isumshft  11633  prodeq1f  11695  prodeq2w  11699  prodeq2  11700  zproddc  11722  fprodm1s  11744  fprodp1s  11745  fprodcom2fi  11769  fprodsplitf  11775  ege2le3  11814  efgt1p2  11838  dfphi2  12358  prmdiveq  12374  pceulem  12432  sloteq  12623  setsslid  12669  ressval2  12684  ecqusaddd  13308  ringidvalg  13457  zrhpropd  14114  metreslem  14548  comet  14667  cnmetdval  14697  lgsdi  15153  lgseisenlem2  15187  redcwlpolemeq1  15544