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

Theorem 3eqtr4g 2340
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 2327 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2333 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  rabeqf  2781  csbeq1  3084  csbeq2d  3105  csbnestgf  3129  difeq1  3287  difeq2  3288  uneq2  3323  ineq2  3364  dfrab3ss  3446  ifeq1  3569  ifeq2  3570  pweq  3628  sneq  3651  csbsng  3692  rabsn  3697  preq1  3706  preq2  3707  tpeq1  3715  tpeq2  3716  tpeq3  3717  prprc1  3736  opeq1  3796  opeq2  3797  oteq1  3805  oteq2  3806  oteq3  3807  csbunig  3835  unieq  3836  inteq  3865  iineq1  3919  iineq2  3922  dfiin2g  3936  iinrab  3964  iinin1  3973  iinxprg  3979  iununi  3986  opabbid  4081  mpteq12f  4096  suceq  4457  xpeq1  4703  xpeq2  4704  csbxpg  4716  rneq  4904  csbrng  4923  reseq1  4949  reseq2  4950  csbresg  4958  resmpt  5000  imaeq1  5007  imaeq2  5008  csbima12gALT  5023  dmpropg  5146  cores  5176  cores2  5185  iotaeq  5227  iotabi  5228  imain  5328  f1oprswap  5515  fveq1  5524  fveq2  5525  csbfv12g  5535  csbfv12gALT  5536  fvres  5542  fnimapr  5583  fvco2  5594  fsnunfv  5720  fsnunres  5721  funiunfv  5774  fliftf  5814  isoini2  5836  oveq  5864  oveq1  5865  oveq2  5866  oprabbid  5901  mpt2eq123  5907  mpt2eq123dva  5909  mpt2eq3dva  5912  resmpt2  5942  ovres  5987  f1ocnvd  6066  ofeq  6080  ofreq  6081  fpar  6222  riotaeqdv  6305  riotabidv  6306  riotabidva  6321  riotaund  6341  onovuni  6359  recseq  6389  tfr2a  6411  rdgeq1  6424  rdgeq2  6425  rdgsucmptf  6441  frsucmpt  6450  seqomeq12  6466  seqomsuc  6469  abianfplem  6470  omopthi  6655  eceq1  6696  eceq2  6697  qseq1  6709  qseq2  6710  uniqs  6719  ecinxp  6734  qsinxp  6735  erovlem  6754  ecopovtrn  6761  ixpeq1  6827  supeq1  7198  supeq2  7201  oieq1  7227  oieq2  7228  ordtypelem1  7233  inf3lemc  7327  cantnfreslem  7377  wemapwe  7400  r1sucg  7441  r1limg  7443  rankprb  7523  karden  7565  cardiun  7615  acneq  7670  alephlim  7694  alephsuc  7695  alephfplem2  7732  dfac2a  7756  infpssrlem2  7930  fin23lem34  7972  fin23lem35  7973  zorn2lem1  8123  zorn2lem7  8129  fpwwe2lem6  8257  fpwwe2lem13  8264  addpiord  8508  mulpiord  8509  addpqnq  8562  mulpqnq  8565  addassnq  8582  mulassnq  8583  distrnq  8585  lterpq  8594  ltexnq  8599  ltsrpr  8699  00sr  8721  recexsrlem  8725  mulgt0sr  8727  addcnsrec  8765  mulcnsrec  8766  negeq  9044  csbnegg  9049  negsubdi  9103  mulneg1  9216  deceq1  10127  deceq2  10128  xnegeq  10534  fseq1p1m1  10857  om2uzrdg  11019  uzrdgsuci  11023  seqeq1  11049  seqeq2  11050  seqeq3  11051  seqfeq4  11095  seqof  11103  hashprg  11368  hashmap  11387  hashbclem  11390  s1eq  11439  cats1co  11506  s2eqd  11512  s3eqd  11513  s4eqd  11514  s5eqd  11515  s6eqd  11516  s7eqd  11517  s8eqd  11518  shftval  11569  limsupgle  11951  lo1eq  12042  rlimeq  12043  sumeq1f  12161  sumeq2w  12165  sumeq2ii  12166  zsum  12191  sumss2  12199  isumclim3  12222  fsumcom2  12237  fsumrev  12241  fsumshft  12242  incexclem  12295  isumshft  12298  ef0lem  12360  ruclem7  12514  sadcp1  12646  smupp1  12671  smueqlem  12681  algrp1  12744  dfphi2  12842  prmdiveq  12854  pceulem  12898  vdwlem6  13033  setsid  13187  elbasfv  13191  elbasov  13192  imastset  13424  imasvscaval  13440  xpscg  13460  isoval  13667  funcoppc  13749  fulloppc  13796  natpropd  13850  catccofval  13932  xpchomfval  13953  xpccofval  13956  grpidpropd  14399  frmdplusg  14476  grpinvpropd  14543  grpsubpropd  14566  grpsubpropd2  14567  mulgpropd  14600  symgplusg  14776  oppgmnd  14827  sylow1lem2  14910  sylow3lem1  14938  prds1  15397  pwsmgp  15401  opprrng  15413  rngidpropd  15477  dvdsrpropd  15478  unitpropd  15479  invrpropd  15480  rhm1  15508  lmhmpropd  15826  lidlrsppropd  15982  lpival  15997  rrgsupp  16032  ressascl  16083  asclpropd  16085  aspval2  16086  psrbas  16124  psrplusg  16126  psrmulr  16129  psrvscafval  16135  resspsrbas  16159  ressmplbas2  16199  opsrle  16217  opsrbaslem  16219  mplrcl  16231  vr1val  16271  psr1rclOLD  16279  ply1rclOLD  16282  ressply1add  16308  ressply1mul  16309  ressply1vsca  16310  psrplusgpropd  16313  mplbaspropd  16314  strov2rcl  16315  psropprmul  16316  ply1baspropd  16321  ply1plusgpropd  16322  ply1sca2  16332  subrgvr1  16338  coe1mul2lem2  16345  zrhpropd  16469  znle  16490  cncmp  17119  2ndcsep  17185  llyeq  17196  nllyeq  17197  xkouni  17294  hmphindis  17488  pt1hmeo  17497  xkocnv  17505  ptcmplem2  17747  snclseqg  17798  prdstmdd  17806  metreslem  17926  comet  18059  nrmmetd  18097  nmpropd  18116  isngp3  18120  ngpds  18125  subgnm  18149  tngnm  18167  idnghm  18252  cnmetdval  18280  cnmpt2pc  18426  htpyco2  18477  phtpyco2  18488  clsocv  18677  ovolunlem1a  18855  voliunlem3  18909  ioombl1lem4  18918  uniioombllem4  18941  itg11  19046  itgeq1f  19126  itgeq2  19132  iblss2  19160  itgss  19166  itgeqa  19168  itgfsum  19181  itgsplit  19190  ditgeq1  19198  ditgeq2  19199  ditgeq3  19200  dvcmulf  19294  dvmptfsum  19322  dvcnvrelem2  19365  mdegfval  19448  mdegpropd  19470  deg1propd  19472  plyeq0  19593  coe11  19634  dgrlt  19647  dgradd2  19649  dgrmulc  19652  dvply1  19664  fta1lem  19687  pserulm  19798  rlimcnp2  20261  jensenlem1  20281  basellem5  20322  dchrbas  20474  dchrrcl  20479  dchrplusg  20486  dchrfi  20494  lgsdi  20571  lgseisenlem2  20589  lgsquadlem3  20595  dchrmusumlema  20642  rpvmasum2  20661  dchrisum0lema  20663  pntlemg  20747  avril1  20836  0vfval  21162  imsval  21254  imsdval  21255  bcseqi  21699  normpythi  21721  cm0  22188  fh1  22197  pjcji  22263  opsqrlem5  22724  pjsdi2i  22737  pjclem3  22777  pjci  22780  golem1  22851  iunrdx  23161  rabbidva2  23164  rnpropg  23189  itgeq12dv  23196  resmptf  23223  gsumpropd2lem  23379  esumeq12dvaf  23414  esumeq2  23418  esumf1o  23429  esumss  23440  esumpfinvalf  23444  ofceq  23458  cvmliftlem5  23820  cvmliftlem10  23825  cvmlift2lem9  23842  cvmliftphtlem  23848  mpteq12d  24128  rdgprc  24151  dfrdg2  24152  predeq1  24169  predeq2  24170  predeq3  24171  trpredeq1  24223  trpredeq2  24224  trpredeq3  24225  symdifeq1  24364  symdifeq2  24365  altopthsn  24495  altxpeq1  24507  altxpeq2  24508  axlowdimlem13  24582  ee7.2aOLD  24900  oprssopvg  25034  prodeq1  25306  prodeq2  25307  prodeq3ii  25308  fprodp1s  25327  limptlimpr2lem1  25574  limptlimpr2lem2  25575  domdomcatfun1  25927  heiborlem4  26538  heiborlem6  26540  imaiinfv  26759  mapfzcons1  26794  rexrabdioph  26875  dnnumch1  27141  dnwech  27145  aomclem6  27156  supeq123d  27158  pwssplit4  27191  frlmplusgval  27229  frlmvscafval  27230  pwfi2f1o  27260  mamudi  27461  mamudir  27462  matval  27465  matrcl  27466  mdetfval  27487  mendplusgfval  27493  mendvscafval  27498  dropab1  27650  dropab2  27651  wallispi2lem2  27821  csbdmg  27980  afveq12d  27996  aoveq123d  28038  aovfundmoveq  28041  aovnuoveq  28051  aovvoveq  28052  aovovn0oveq  28054  isusgra0  28106  bnj956  28808  bnj1385  28865  bnj96  28897  bnj548  28929  bnj553  28930  bnj554  28931  bnj602  28947  bnj18eq1  28959  bnj1234  29043  bnj1296  29051  bnj1318  29055  bnj1442  29079  bnj1450  29080  toycom  29162  ldualvbase  29316  ldualfvadd  29318  ldualsca  29322  ldualsbase  29323  ldualsaddN  29324  ldualfvs  29326  ldual0  29337  ldual1  29338  ldualneg  29339  cdleme19f  30497  cdleme20m  30512  cdleme21k  30527  cdleme27b  30557  cdleme31so  30568  cdleme31sn  30569  cdleme31se  30571  cdleme31se2  30572  cdleme31sc  30573  cdleme31sde  30574  cdleme31fv  30579  cdleme40v  30658  cdleme43dN  30681  cdlemeg46ngfr  30707  ltrnco4  30928  tgrpbase  30935  tgrpopr  30936  erngbase  30990  erngfplus  30991  erngfmul  30994  erngbase-rN  30998  erngfplus-rN  30999  erngfmul-rN  31002  dvasca  31195  dvavbase  31202  dvafvadd  31203  dvafvsca  31205  tendocnv  31211  dvhsca  31272  dvhfplusr  31274  dvhvbase  31277  dvhfvadd  31281  dvhfvsca  31290  lcdvadd  31787  lcdsbase  31790  lcdsadd  31791  lcdvs  31793  lcd0  31798  lcd1  31799  lcdneg  31800  mapdvalc  31819  mapdval4N  31822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator