MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr4g Structured version   Unicode version

Theorem 3eqtr4g 2492
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
StepHypRef Expression
1 3eqtr4g.2 . . 3  |-  C  =  A
2 3eqtr4g.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2syl5eq 2479 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2485 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  rabeqf  2941  csbeq1  3246  csbeq2d  3267  csbnestgf  3291  difeq1  3450  difeq2  3451  uneq2  3487  ineq2  3528  dfrab3ss  3611  ifeq1  3735  ifeq2  3736  pweq  3794  sneq  3817  csbsng  3859  rabsn  3865  preq1  3875  preq2  3876  tpeq1  3884  tpeq2  3885  tpeq3  3886  prprc1  3906  opeq1  3976  opeq2  3977  oteq1  3985  oteq2  3986  oteq3  3987  csbunig  4015  unieq  4016  inteq  4045  iineq1  4099  iineq2  4102  dfiin2g  4116  iinrab  4145  iinin1  4154  iinxprg  4160  iununi  4167  opabbid  4262  mpteq12f  4277  suceq  4638  xpeq1  4884  xpeq2  4885  csbxpg  4897  rneq  5087  csbrng  5106  reseq1  5132  reseq2  5133  csbresg  5141  resmpt  5183  imaeq1  5190  imaeq2  5191  csbima12gALT  5206  dmpropg  5335  cores  5365  cores2  5374  xpco  5406  iotaeq  5418  iotabi  5419  fntpg  5498  imain  5521  f1oprswap  5709  fveq1  5719  fveq2  5720  csbfv12g  5730  csbfv12gALT  5731  fvres  5737  fnimapr  5779  fvco2  5790  fsnunfv  5925  fsnunres  5926  funiunfv  5987  fliftf  6029  isoini2  6051  oveq  6079  oveq1  6080  oveq2  6081  oprabbid  6119  mpt2eq123  6125  mpt2eq123dva  6127  mpt2eq3dva  6130  resmpt2  6160  ovres  6205  f1ocnvd  6285  ofeq  6299  ofreq  6300  fpar  6442  riotaeqdv  6542  riotabidv  6543  riotabidva  6558  riotaund  6578  onovuni  6596  recseq  6626  tfr2a  6648  rdgeq1  6661  rdgeq2  6662  rdgsucmptf  6678  frsucmpt  6687  seqomeq12  6703  seqomsuc  6706  abianfplem  6707  omopthi  6892  eceq1  6933  eceq2  6934  qseq1  6946  qseq2  6947  uniqs  6956  ecinxp  6971  qsinxp  6972  erovlem  6992  ecopovtrn  6999  ixpeq1  7065  supeq1  7442  supeq2  7445  supeq3  7446  supeq123d  7447  oieq1  7473  oieq2  7474  ordtypelem1  7479  inf3lemc  7573  cantnfreslem  7623  wemapwe  7646  r1sucg  7687  r1limg  7689  rankprb  7769  karden  7811  cardiun  7861  acneq  7916  alephlim  7940  alephsuc  7941  alephfplem2  7978  dfac2a  8002  infpssrlem2  8176  fin23lem34  8218  fin23lem35  8219  zorn2lem1  8368  zorn2lem7  8374  fpwwe2lem6  8502  fpwwe2lem13  8509  addpiord  8753  mulpiord  8754  addpqnq  8807  mulpqnq  8810  addassnq  8827  mulassnq  8828  distrnq  8830  lterpq  8839  ltexnq  8844  ltsrpr  8944  00sr  8966  recexsrlem  8970  mulgt0sr  8972  addcnsrec  9010  mulcnsrec  9011  negeq  9290  csbnegg  9295  negsubdi  9349  mulneg1  9462  deceq1  10377  deceq2  10378  xnegeq  10785  fseq1p1m1  11114  om2uzrdg  11288  uzrdgsuci  11292  seqeq1  11318  seqeq2  11319  seqeq3  11320  seqfeq4  11364  seqof  11372  hashprg  11658  hashtpg  11683  hashmap  11690  hashbclem  11693  s1eq  11745  cats1co  11812  s2eqd  11818  s3eqd  11819  s4eqd  11820  s5eqd  11821  s6eqd  11822  s7eqd  11823  s8eqd  11824  shftval  11881  limsupgle  12263  lo1eq  12354  rlimeq  12355  sumeq1f  12474  sumeq2w  12478  sumeq2ii  12479  zsum  12504  sumss2  12512  isumclim3  12535  fsumcom2  12550  fsumrev  12554  fsumshft  12555  incexclem  12608  incexc2  12610  isumshft  12611  ef0lem  12673  ruclem7  12827  sadcp1  12959  smupp1  12984  smueqlem  12994  algrp1  13057  dfphi2  13155  prmdiveq  13167  pceulem  13211  vdwlem6  13346  setsid  13500  elbasfv  13504  elbasov  13505  imastset  13739  imasvscaval  13755  xpscg  13775  isoval  13982  funcoppc  14064  fulloppc  14111  fuccofval  14148  natpropd  14165  catccofval  14247  xpchomfval  14268  xpccofval  14271  grpidpropd  14714  frmdplusg  14791  grpinvpropd  14858  grpsubpropd  14881  grpsubpropd2  14882  mulgpropd  14915  symgplusg  15091  oppgmnd  15142  sylow1lem2  15225  sylow3lem1  15253  prds1  15712  pwsmgp  15716  opprrng  15728  rngidpropd  15792  dvdsrpropd  15793  unitpropd  15794  invrpropd  15795  rhm1  15823  lmhmpropd  16137  lidlrsppropd  16293  lpival  16308  rrgsupp  16343  ressascl  16394  asclpropd  16396  aspval2  16397  psrbas  16435  psrplusg  16437  psrmulr  16440  psrvscafval  16446  resspsrbas  16470  ressmplbas2  16510  opsrle  16528  opsrbaslem  16530  mplrcl  16542  vr1val  16582  ressply1add  16616  ressply1mul  16617  ressply1vsca  16618  psrplusgpropd  16621  mplbaspropd  16622  strov2rcl  16623  psropprmul  16624  ply1baspropd  16629  ply1plusgpropd  16630  ply1sca2  16640  subrgvr1  16646  coe1mul2lem2  16653  zrhpropd  16788  znle  16809  cncmp  17447  2ndcsep  17514  llyeq  17525  nllyeq  17526  xkouni  17623  hmphindis  17821  pt1hmeo  17830  xkocnv  17838  ptcmplem2  18076  snclseqg  18137  prdstmdd  18145  ustexsym  18237  ucnextcn  18326  metreslem  18384  comet  18535  nrmmetd  18614  nmpropd  18633  isngp3  18637  ngpds  18642  subgnm  18666  tngnm  18684  idnghm  18769  cnmetdval  18797  cnmpt2pc  18945  htpyco2  18996  phtpyco2  19007  clsocv  19196  ovolunlem1a  19384  voliunlem3  19438  ioombl1lem4  19447  uniioombllem4  19470  itg11  19575  itgeq1f  19655  itgeq2  19661  iblss2  19689  itgss  19695  itgeqa  19697  itgfsum  19710  itgsplit  19719  ditgeq1  19727  ditgeq2  19728  ditgeq3  19729  dvcmulf  19823  dvmptfsum  19851  dvcnvrelem2  19894  mdegfval  19977  mdegpropd  19999  deg1propd  20001  plyeq0  20122  coe11  20163  dgrlt  20176  dgradd2  20178  dgrmulc  20181  dvply1  20193  fta1lem  20216  pserulm  20330  rlimcnp2  20797  jensenlem1  20817  basellem5  20859  dchrbas  21011  dchrrcl  21016  dchrplusg  21023  dchrfi  21031  lgsdi  21108  lgseisenlem2  21126  lgsquadlem3  21132  dchrmusumlema  21179  rpvmasum2  21198  dchrisum0lema  21200  pntlemg  21284  isusgra0  21368  nbgraf1olem5  21447  nb3graprlem1  21452  constr2spthlem1  21586  constr3pthlem1  21634  constr3pthlem2  21635  avril1  21749  0vfval  22077  imsval  22169  imsdval  22170  bcseqi  22614  normpythi  22636  cm0  23103  fh1  23112  pjcji  23178  opsqrlem5  23639  pjsdi2i  23652  pjclem3  23692  pjci  23695  golem1  23766  rabbidva2  23978  iunrdx  24006  rnpropg  24027  mptcnv  24037  ofresid  24047  resmptf  24063  gsumpropd2lem  24212  rhmopp  24249  xrge0mulc1cn  24319  qqhval2  24358  esumeq12dvaf  24420  esumeq2  24425  esumf1o  24437  esumfzf  24451  esumss  24454  esumpfinvalf  24458  ofceq  24472  itgeq12dv  24633  cvmliftlem5  24968  cvmliftlem10  24973  cvmlift2lem9  24990  cvmliftphtlem  24996  prodeq1f  25226  prodeq2w  25230  prodeq2ii  25231  zprod  25255  fprodm1s  25285  fprodp1s  25286  fprodshft  25292  fprodrev  25293  fprodcom2  25300  iprodclim3  25305  mpteq12d  25388  rdgprc  25414  dfrdg2  25415  predeq123  25432  trpredeq1  25490  trpredeq2  25491  trpredeq3  25492  wrecseq123  25524  wsuceq123  25557  wlimeq12  25562  symdifeq1  25657  symdifeq2  25658  altopthsn  25798  altxpeq1  25810  altxpeq2  25811  axlowdimlem13  25885  ee7.2aOLD  26203  mbfposadd  26244  cnambfre  26245  iblabsnclem  26258  ftc1anclem1  26270  heiborlem4  26514  heiborlem6  26516  imaiinfv  26731  mapfzcons1  26764  rexrabdioph  26845  dnnumch1  27110  dnwech  27114  aomclem6  27125  pwssplit4  27159  frlmplusgval  27197  frlmvscafval  27198  pwfi2f1o  27228  mamudi  27429  mamudir  27430  matrcl  27434  mdetfval  27455  mendplusgfval  27461  mendvscafval  27466  dropab1  27617  dropab2  27618  itgsinexplem1  27715  wallispi2lem2  27788  csbdmg  27949  afveq12d  27964  aoveq123d  28009  aovfundmoveq  28012  aovnuoveq  28022  aovvoveq  28023  aovovn0oveq  28025  resisresindm  28061  cshwsiun  28249  bnj956  29084  bnj1385  29141  bnj96  29173  bnj548  29205  bnj553  29206  bnj554  29207  bnj602  29223  bnj18eq1  29235  bnj1234  29319  bnj1296  29327  bnj1318  29331  bnj1442  29355  bnj1450  29356  toycom  29707  ldualvbase  29861  ldualfvadd  29863  ldualsca  29867  ldualsbase  29868  ldualsaddN  29869  ldualfvs  29871  ldual0  29882  ldual1  29883  ldualneg  29884  cdleme19f  31042  cdleme20m  31057  cdleme21k  31072  cdleme27b  31102  cdleme31so  31113  cdleme31sn  31114  cdleme31se  31116  cdleme31se2  31117  cdleme31sc  31118  cdleme31sde  31119  cdleme31fv  31124  cdleme40v  31203  cdleme43dN  31226  cdlemeg46ngfr  31252  ltrnco4  31473  tgrpbase  31480  tgrpopr  31481  erngbase  31535  erngfplus  31536  erngfmul  31539  erngbase-rN  31543  erngfplus-rN  31544  erngfmul-rN  31547  dvasca  31740  dvavbase  31747  dvafvadd  31748  dvafvsca  31750  tendocnv  31756  dvhsca  31817  dvhfplusr  31819  dvhvbase  31822  dvhfvadd  31826  dvhfvsca  31835  lcdvadd  32332  lcdsbase  32335  lcdsadd  32336  lcdvs  32338  lcd0  32343  lcd1  32344  lcdneg  32345  mapdvalc  32364  mapdval4N  32367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator