Theorem 3eqtr4g 2495

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

Hypotheses

Ref	Expression
3eqtr4g.1	|- ( ph -> A = B )
3eqtr4g.2	|- C = A
3eqtr4g.3	|- D = B

Assertion

Ref	Expression
3eqtr4g	|- ( ph -> C = D )

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 |- C = A
2		3eqtr4g.1	. . 3 |- ( ph -> A = B )
3	1, 2	syl5eq 2482	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	syl6eqr 2488	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431

This theorem is referenced by:  rabbidva2  2957  rabeqf  2960  csbeq1  3286  difeq1  3462  difeq2  3463  uneq2  3499  ineq2  3541  dfrab3ss  3623  csbeq2d  3681  csbnestgf  3687  ifeq1  3790  ifeq2  3791  pweq  3858  sneq  3882  csbsng  3930  rabsn  3937  preq1  3949  preq2  3950  tpeq1  3958  tpeq2  3959  tpeq3  3960  prprc1  3980  opeq1  4054  opeq2  4055  oteq1  4063  oteq2  4064  oteq3  4065  unieq  4094  csbuni  4114  csbunigOLD  4115  inteq  4126  iineq1  4180  iineq2  4183  dfiin2g  4198  iinrab  4227  iinin1  4236  iinxprg  4243  iununi  4250  opabbid  4349  mpteq12f  4363  csbmpt12  4617  suceq  4779  xpeq1  4849  xpeq2  4850  csbxpgOLD  4914  rneq  5060  reseq1  5099  reseq2  5100  csbresgOLD  5109  resmpt  5151  imaeq1  5159  imaeq2  5160  mptcnv  5234  csbrngOLD  5295  dmpropg  5307  rnpropg  5314  cores  5336  cores2  5345  xpco  5372  iotaeq  5384  iotabi  5385  fntpg  5468  imain  5489  f1oprswap  5675  fveq1  5685  fveq2  5686  fvres  5699  csbfv12  5720  csbfv12gOLD  5721  fnimapr  5750  fvco2  5761  residpr  5881  fsnunfv  5913  fsnunres  5914  funiunfv  5960  fliftf  6003  isoini2  6025  riotaeqdv  6048  riotabidv  6049  riotauni  6053  riotabidva  6064  snriota  6077  oveq  6092  oveq1  6093  oveq2  6094  oprabbid  6134  mpt2eq123  6140  mpt2eq123dva  6142  mpt2eq3dva  6145  resmpt2  6183  ovres  6225  f1ocnvd  6304  ofeq  6317  ofreq  6318  fpar  6671  extmptsuppeq  6708  onovuni  6795  recseq  6825  tfr2a  6846  rdgeq1  6859  rdgeq2  6860  rdgsucmptf  6876  frsucmpt  6885  seqomeq12  6901  seqomsuc  6904  omopthi  7088  eceq1  7129  eceq2  7130  qseq1  7142  qseq2  7143  uniqs  7152  ecinxp  7167  qsinxp  7168  erovlem  7188  ecopovtrn  7195  ixpeq1  7266  supeq1  7687  supeq2  7690  supeq3  7691  supeq123d  7692  oieq1  7718  oieq2  7719  ordtypelem1  7724  inf3lemc  7824  wemapwe  7920  wemapweOLD  7921  r1sucg  7968  r1limg  7970  rankprb  8050  karden  8094  cardiun  8144  acneq  8205  alephlim  8229  alephsuc  8230  alephfplem2  8267  dfac2a  8291  infpssrlem2  8465  fin23lem34  8507  fin23lem35  8508  zorn2lem1  8657  zorn2lem7  8663  fpwwe2lem6  8794  fpwwe2lem13  8801  addpiord  9045  mulpiord  9046  addpqnq  9099  mulpqnq  9102  addassnq  9119  mulassnq  9120  distrnq  9122  lterpq  9131  ltexnq  9136  ltsrpr  9236  00sr  9258  recexsrlem  9262  mulgt0sr  9264  addcnsrec  9302  mulcnsrec  9303  negeq  9594  csbnegg  9599  negsubdi  9657  mulneg1  9773  deceq1  10750  deceq2  10751  xnegeq  11169  fseq1p1m1  11526  om2uzrdg  11771  uzrdgsuci  11775  seqeq1  11801  seqeq2  11802  seqeq3  11803  seqfeq4  11847  seqof  11855  hashprg  12147  hashtpg  12178  hashmap  12189  hashbclem  12197  csbwrdg  12249  s1eq  12283  cats1co  12475  s2eqd  12481  s3eqd  12482  s4eqd  12483  s5eqd  12484  s6eqd  12485  s7eqd  12486  s8eqd  12487  shftval  12555  limsupgle  12947  lo1eq  13038  rlimeq  13039  sumeq1  13158  sumeq2w  13161  sumeq2ii  13162  zsum  13187  sumss2  13195  isumclim3  13218  fsumcom2  13233  fsumrev  13238  incexclem  13291  incexc2  13293  isumshft  13294  ef0lem  13356  ruclem7  13510  sadcp1  13643  smupp1  13668  smueqlem  13678  algrp1  13741  dfphi2  13841  prmdiveq  13853  pceulem  13904  vdwlem6  14039  cshwsiun  14118  setsid  14207  elbasfv  14213  elbasov  14214  imastset  14452  imasvscaval  14468  xpscg  14488  isoval  14695  funcoppc  14777  fulloppc  14824  fuccofval  14861  natpropd  14878  catccofval  14960  xpchomfval  14981  xpccofval  14984  lubfval  15140  glbfval  15153  grpidpropd  15439  gsumpropd2lem  15496  frmdplusg  15523  grpinvpropd  15592  grpsubpropd  15617  grpsubpropd2  15618  mulgpropd  15651  oppgmnd  15860  symgplusg  15885  sylow1lem2  16089  sylow3lem1  16117  prds1  16694  pwsmgp  16698  opprrng  16711  rngidpropd  16775  dvdsrpropd  16776  unitpropd  16777  invrpropd  16778  rhm1  16806  lmhmpropd  17131  lidlrsppropd  17289  lpival  17304  rrgsuppOLD  17340  ressascl  17391  asclpropd  17393  aspval2  17394  psrbas  17425  psrbasOLD  17426  psrplusg  17429  psrmulr  17432  psrvscafval  17438  resspsrbas  17464  ressmplbas2  17511  opsrle  17532  opsrbaslem  17534  mplrcl  17546  vr1val  17623  ressply1add  17659  ressply1mul  17660  ressply1vsca  17661  psrplusgpropd  17665  mplbaspropd  17666  strov2rcl  17667  psropprmul  17668  ply1baspropd  17673  ply1plusgpropd  17674  ply1sca2  17684  subrgvr1  17690  coe1mul2lem2  17697  zrhpropd  17921  znle  17942  frlmplusgval  18166  frlmvscafval  18168  mamudi  18282  mamudir  18283  matrcl  18287  oftpos  18308  mattpos1  18315  mdetfval  18372  mdetrlin  18384  mdetrsca  18385  mdetrsca2  18386  mdetrlin2  18388  mdetunilem5  18397  madufval  18418  madugsum  18424  cncmp  18970  2ndcsep  19038  llyeq  19049  nllyeq  19050  xkouni  19147  hmphindis  19345  pt1hmeo  19354  xkocnv  19362  ptcmplem2  19600  snclseqg  19661  prdstmdd  19669  ustexsym  19765  ucnextcn  19854  metreslem  19912  comet  20063  nrmmetd  20142  nmpropd  20161  isngp3  20165  ngpds  20170  subgnm  20194  tngnm  20212  idnghm  20297  cnmetdval  20325  cnmpt2pc  20475  htpyco2  20526  phtpyco2  20537  clsocv  20737  ovolunlem1a  20954  voliunlem3  21008  ioombl1lem4  21017  uniioombllem4  21041  itg11  21144  itgeq1f  21224  itgeq2  21230  iblss2  21258  itgss  21264  itgeqa  21266  itgfsum  21279  itgsplit  21288  ditgeq1  21298  ditgeq2  21299  ditgeq3  21300  dvcmulf  21394  dvmptfsum  21422  dvcnvrelem2  21465  mdegfval  21506  mdegpropd  21530  deg1propd  21532  plyeq0  21654  coe11  21695  dgrlt  21708  dgradd2  21710  dgrmulc  21713  dvply1  21725  fta1lem  21748  pserulm  21862  rlimcnp2  22335  jensenlem1  22355  basellem5  22397  dchrbas  22549  dchrrcl  22554  dchrplusg  22561  dchrfi  22569  lgsdi  22646  lgseisenlem2  22664  lgsquadlem3  22670  dchrmusumlema  22717  rpvmasum2  22736  dchrisum0lema  22738  pntlemg  22822  axlowdimlem13  23151  isusgra0  23226  nbgraf1olem5  23305  nb3graprlem1  23310  constr2spthlem1  23444  constr3pthlem1  23492  constr3pthlem2  23493  avril1  23607  0vfval  23935  imsval  24027  imsdval  24028  bcseqi  24473  normpythi  24495  cm0  24963  fh1  24972  pjcji  25038  opsqrlem5  25499  pjsdi2i  25512  pjclem3  25552  pjci  25555  golem1  25626  iunrdx  25865  ofresid  25911  resmptf  25925  f1od2  25975  rhmopp  26238  resv1r  26257  xrge0mulc1cn  26323  qqhval2  26363  esumeq12dvaf  26439  esumeq2  26444  esumf1o  26456  esumfzf  26470  esumss  26473  esumpfinvalf  26477  ofceq  26491  itgeq12dv  26664  ccatmulgnn0dir  26892  cvmliftlem5  27130  cvmliftlem10  27135  cvmlift2lem9  27152  cvmliftphtlem  27158  prodeq1f  27372  prodeq2w  27376  prodeq2ii  27377  zprod  27401  fprodm1s  27431  fprodp1s  27432  fprodshft  27438  fprodrev  27439  fprodcom2  27446  iprodclim3  27451  mpteq12d  27534  rdgprc  27559  dfrdg2  27560  predeq123  27577  trpredeq1  27635  trpredeq2  27636  trpredeq3  27637  wrecseq123  27669  wsuceq123  27702  wlimeq12  27707  symdifeq1  27802  symdifeq2  27803  altopthsn  27943  altxpeq1  27955  altxpeq2  27956  ee7.2aOLD  28259  finixpnum  28367  ptrest  28378  mbfposadd  28392  cnambfre  28393  iblabsnclem  28408  ftc1anclem1  28420  heiborlem4  28666  heiborlem6  28668  mpt2bi123f  28928  iineq12f  28930  mptbi12f  28932  imaiinfv  28982  mapfzcons1  29006  rexrabdioph  29085  dnnumch1  29350  dnwech  29354  aomclem6  29365  pwssplit4  29395  pwfi2f1o  29404  mendplusgfval  29495  mendvscafval  29500  dropab1  29656  dropab2  29657  itgsinexplem1  29747  wallispi2lem2  29820  afveq12d  29992  aoveq123d  30037  aovfundmoveq  30040  aovnuoveq  30050  aovvoveq  30051  aovovn0oveq  30053  csbprg  30070  resisresindm  30092  fsumsplitsndif  30191  fsumsplitsnun  30195  wwlkextwrd  30313  rusgranumwlkl1  30512  rusgranumwlklem3  30522  numclwwlkovf2  30630  xpprsng  30671  csbfv12gALTOLD  31444  csbima12gALTOLD  31445  bnj956  31657  bnj1385  31713  bnj96  31745  bnj548  31777  bnj553  31778  bnj554  31779  bnj602  31795  bnj18eq1  31807  bnj1234  31891  bnj1296  31899  bnj1318  31903  bnj1442  31927  bnj1450  31928  bj-rabbida2  32269  bj-sngleq  32307  bj-tageq  32316  bj-projeq  32332  bj-projval  32336  bj-1upleq  32339  bj-pr1eq  32342  bj-pr2eq  32356  riotaclbgBAD  32445  riotaclbBAD  32446  toycom  32458  ldualvbase  32611  ldualfvadd  32613  ldualsca  32617  ldualsbase  32618  ldualsaddN  32619  ldualfvs  32621  ldual0  32632  ldual1  32633  ldualneg  32634  cdleme19f  33792  cdleme20m  33807  cdleme21k  33822  cdleme27b  33852  cdleme31so  33863  cdleme31sn  33864  cdleme31se  33866  cdleme31se2  33867  cdleme31sc  33868  cdleme31sde  33869  cdleme31fv  33874  cdleme40v  33953  cdleme43dN  33976  cdlemeg46ngfr  34002  ltrnco4  34223  tgrpbase  34230  tgrpopr  34231  erngbase  34285  erngfplus  34286  erngfmul  34289  erngbase-rN  34293  erngfplus-rN  34294  erngfmul-rN  34297  dvasca  34490  dvavbase  34497  dvafvadd  34498  dvafvsca  34500  tendocnv  34506  dvhsca  34567  dvhfplusr  34569  dvhvbase  34572  dvhfvadd  34576  dvhfvsca  34585  lcdvadd  35082  lcdsbase  35085  lcdsadd  35086  lcdvs  35088  lcd0  35093  lcd1  35094  lcdneg  35095  mapdvalc  35114  mapdval4N  35117