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

Theorem 3eqtr4g 2353
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 2340 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2346 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  rabeqf  2794  csbeq1  3097  csbeq2d  3118  csbnestgf  3142  difeq1  3300  difeq2  3301  uneq2  3336  ineq2  3377  dfrab3ss  3459  ifeq1  3582  ifeq2  3583  pweq  3641  sneq  3664  csbsng  3705  rabsn  3710  preq1  3719  preq2  3720  tpeq1  3728  tpeq2  3729  tpeq3  3730  prprc1  3749  opeq1  3812  opeq2  3813  oteq1  3821  oteq2  3822  oteq3  3823  csbunig  3851  unieq  3852  inteq  3881  iineq1  3935  iineq2  3938  dfiin2g  3952  iinrab  3980  iinin1  3989  iinxprg  3995  iununi  4002  opabbid  4097  mpteq12f  4112  suceq  4473  xpeq1  4719  xpeq2  4720  csbxpg  4732  rneq  4920  csbrng  4939  reseq1  4965  reseq2  4966  csbresg  4974  resmpt  5016  imaeq1  5023  imaeq2  5024  csbima12gALT  5039  dmpropg  5162  cores  5192  cores2  5201  iotaeq  5243  iotabi  5244  imain  5344  f1oprswap  5531  fveq1  5540  fveq2  5541  csbfv12g  5551  csbfv12gALT  5552  fvres  5558  fnimapr  5599  fvco2  5610  fsnunfv  5736  fsnunres  5737  funiunfv  5790  fliftf  5830  isoini2  5852  oveq  5880  oveq1  5881  oveq2  5882  oprabbid  5917  mpt2eq123  5923  mpt2eq123dva  5925  mpt2eq3dva  5928  resmpt2  5958  ovres  6003  f1ocnvd  6082  ofeq  6096  ofreq  6097  fpar  6238  riotaeqdv  6321  riotabidv  6322  riotabidva  6337  riotaund  6357  onovuni  6375  recseq  6405  tfr2a  6427  rdgeq1  6440  rdgeq2  6441  rdgsucmptf  6457  frsucmpt  6466  seqomeq12  6482  seqomsuc  6485  abianfplem  6486  omopthi  6671  eceq1  6712  eceq2  6713  qseq1  6725  qseq2  6726  uniqs  6735  ecinxp  6750  qsinxp  6751  erovlem  6770  ecopovtrn  6777  ixpeq1  6843  supeq1  7214  supeq2  7217  oieq1  7243  oieq2  7244  ordtypelem1  7249  inf3lemc  7343  cantnfreslem  7393  wemapwe  7416  r1sucg  7457  r1limg  7459  rankprb  7539  karden  7581  cardiun  7631  acneq  7686  alephlim  7710  alephsuc  7711  alephfplem2  7748  dfac2a  7772  infpssrlem2  7946  fin23lem34  7988  fin23lem35  7989  zorn2lem1  8139  zorn2lem7  8145  fpwwe2lem6  8273  fpwwe2lem13  8280  addpiord  8524  mulpiord  8525  addpqnq  8578  mulpqnq  8581  addassnq  8598  mulassnq  8599  distrnq  8601  lterpq  8610  ltexnq  8615  ltsrpr  8715  00sr  8737  recexsrlem  8741  mulgt0sr  8743  addcnsrec  8781  mulcnsrec  8782  negeq  9060  csbnegg  9065  negsubdi  9119  mulneg1  9232  deceq1  10143  deceq2  10144  xnegeq  10550  fseq1p1m1  10873  om2uzrdg  11035  uzrdgsuci  11039  seqeq1  11065  seqeq2  11066  seqeq3  11067  seqfeq4  11111  seqof  11119  hashprg  11384  hashmap  11403  hashbclem  11406  s1eq  11455  cats1co  11522  s2eqd  11528  s3eqd  11529  s4eqd  11530  s5eqd  11531  s6eqd  11532  s7eqd  11533  s8eqd  11534  shftval  11585  limsupgle  11967  lo1eq  12058  rlimeq  12059  sumeq1f  12177  sumeq2w  12181  sumeq2ii  12182  zsum  12207  sumss2  12215  isumclim3  12238  fsumcom2  12253  fsumrev  12257  fsumshft  12258  incexclem  12311  isumshft  12314  ef0lem  12376  ruclem7  12530  sadcp1  12662  smupp1  12687  smueqlem  12697  algrp1  12760  dfphi2  12858  prmdiveq  12870  pceulem  12914  vdwlem6  13049  setsid  13203  elbasfv  13207  elbasov  13208  imastset  13440  imasvscaval  13456  xpscg  13476  isoval  13683  funcoppc  13765  fulloppc  13812  natpropd  13866  catccofval  13948  xpchomfval  13969  xpccofval  13972  grpidpropd  14415  frmdplusg  14492  grpinvpropd  14559  grpsubpropd  14582  grpsubpropd2  14583  mulgpropd  14616  symgplusg  14792  oppgmnd  14843  sylow1lem2  14926  sylow3lem1  14954  prds1  15413  pwsmgp  15417  opprrng  15429  rngidpropd  15493  dvdsrpropd  15494  unitpropd  15495  invrpropd  15496  rhm1  15524  lmhmpropd  15842  lidlrsppropd  15998  lpival  16013  rrgsupp  16048  ressascl  16099  asclpropd  16101  aspval2  16102  psrbas  16140  psrplusg  16142  psrmulr  16145  psrvscafval  16151  resspsrbas  16175  ressmplbas2  16215  opsrle  16233  opsrbaslem  16235  mplrcl  16247  vr1val  16287  psr1rclOLD  16295  ply1rclOLD  16298  ressply1add  16324  ressply1mul  16325  ressply1vsca  16326  psrplusgpropd  16329  mplbaspropd  16330  strov2rcl  16331  psropprmul  16332  ply1baspropd  16337  ply1plusgpropd  16338  ply1sca2  16348  subrgvr1  16354  coe1mul2lem2  16361  zrhpropd  16485  znle  16506  cncmp  17135  2ndcsep  17201  llyeq  17212  nllyeq  17213  xkouni  17310  hmphindis  17504  pt1hmeo  17513  xkocnv  17521  ptcmplem2  17763  snclseqg  17814  prdstmdd  17822  metreslem  17942  comet  18075  nrmmetd  18113  nmpropd  18132  isngp3  18136  ngpds  18141  subgnm  18165  tngnm  18183  idnghm  18268  cnmetdval  18296  cnmpt2pc  18442  htpyco2  18493  phtpyco2  18504  clsocv  18693  ovolunlem1a  18871  voliunlem3  18925  ioombl1lem4  18934  uniioombllem4  18957  itg11  19062  itgeq1f  19142  itgeq2  19148  iblss2  19176  itgss  19182  itgeqa  19184  itgfsum  19197  itgsplit  19206  ditgeq1  19214  ditgeq2  19215  ditgeq3  19216  dvcmulf  19310  dvmptfsum  19338  dvcnvrelem2  19381  mdegfval  19464  mdegpropd  19486  deg1propd  19488  plyeq0  19609  coe11  19650  dgrlt  19663  dgradd2  19665  dgrmulc  19668  dvply1  19680  fta1lem  19703  pserulm  19814  rlimcnp2  20277  jensenlem1  20297  basellem5  20338  dchrbas  20490  dchrrcl  20495  dchrplusg  20502  dchrfi  20510  lgsdi  20587  lgseisenlem2  20605  lgsquadlem3  20611  dchrmusumlema  20658  rpvmasum2  20677  dchrisum0lema  20679  pntlemg  20763  avril1  20852  0vfval  21178  imsval  21270  imsdval  21271  bcseqi  21715  normpythi  21737  cm0  22204  fh1  22213  pjcji  22279  opsqrlem5  22740  pjsdi2i  22753  pjclem3  22793  pjci  22796  golem1  22867  iunrdx  23177  rabbidva2  23180  rnpropg  23205  itgeq12dv  23211  resmptf  23238  gsumpropd2lem  23394  esumeq12dvaf  23429  esumeq2  23433  esumf1o  23444  esumss  23455  esumpfinvalf  23459  ofceq  23473  cvmliftlem5  23835  cvmliftlem10  23840  cvmlift2lem9  23857  cvmliftphtlem  23863  faclim  24126  cprodeq1f  24130  cprodeq2w  24134  cprodeq2ii  24135  zprod  24160  mpteq12d  24199  rdgprc  24222  dfrdg2  24223  predeq1  24240  predeq2  24241  predeq3  24242  trpredeq1  24294  trpredeq2  24295  trpredeq3  24296  symdifeq1  24435  symdifeq2  24436  altopthsn  24567  altxpeq1  24579  altxpeq2  24580  axlowdimlem13  24654  ee7.2aOLD  24972  iblabsnclem  25014  oprssopvg  25137  prodeq1  25409  prodeq2  25410  prodeq3ii  25411  fprodp1s  25430  limptlimpr2lem1  25677  limptlimpr2lem2  25678  domdomcatfun1  26030  heiborlem4  26641  heiborlem6  26643  imaiinfv  26862  mapfzcons1  26897  rexrabdioph  26978  dnnumch1  27244  dnwech  27248  aomclem6  27259  supeq123d  27261  pwssplit4  27294  frlmplusgval  27332  frlmvscafval  27333  pwfi2f1o  27363  mamudi  27564  mamudir  27565  matval  27568  matrcl  27569  mdetfval  27590  mendplusgfval  27596  mendvscafval  27601  dropab1  27753  dropab2  27754  wallispi2lem2  27924  csbdmg  28085  afveq12d  28101  aoveq123d  28146  aovfundmoveq  28149  aovnuoveq  28159  aovvoveq  28160  aovovn0oveq  28162  hashtpg  28217  isusgra0  28238  nb3graprlem1  28287  constr3pthlem1  28401  constr3pthlem2  28402  bnj956  29124  bnj1385  29181  bnj96  29213  bnj548  29245  bnj553  29246  bnj554  29247  bnj602  29263  bnj18eq1  29275  bnj1234  29359  bnj1296  29367  bnj1318  29371  bnj1442  29395  bnj1450  29396  toycom  29784  ldualvbase  29938  ldualfvadd  29940  ldualsca  29944  ldualsbase  29945  ldualsaddN  29946  ldualfvs  29948  ldual0  29959  ldual1  29960  ldualneg  29961  cdleme19f  31119  cdleme20m  31134  cdleme21k  31149  cdleme27b  31179  cdleme31so  31190  cdleme31sn  31191  cdleme31se  31193  cdleme31se2  31194  cdleme31sc  31195  cdleme31sde  31196  cdleme31fv  31201  cdleme40v  31280  cdleme43dN  31303  cdlemeg46ngfr  31329  ltrnco4  31550  tgrpbase  31557  tgrpopr  31558  erngbase  31612  erngfplus  31613  erngfmul  31616  erngbase-rN  31620  erngfplus-rN  31621  erngfmul-rN  31624  dvasca  31817  dvavbase  31824  dvafvadd  31825  dvafvsca  31827  tendocnv  31833  dvhsca  31894  dvhfplusr  31896  dvhvbase  31899  dvhfvadd  31903  dvhfvsca  31912  lcdvadd  32409  lcdsbase  32412  lcdsadd  32413  lcdvs  32415  lcd0  32420  lcd1  32421  lcdneg  32422  mapdvalc  32441  mapdval4N  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator