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

Theorem 3eqtr4g 2530
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 21-Jun-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 2517 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4g.3 . 2  |-  D  =  B
53, 4syl6eqr 2523 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-cleq 2464
This theorem is referenced by:  rabbidva2  3020  rabeqf  3023  csbeq1  3352  csbeq2  3353  difeq1  3533  difeq2  3534  uneq2  3573  ineq2  3619  symdifeq1  3656  symdifeq2  3657  dfrab3ss  3712  csbeq2d  3784  csbnestgf  3789  ifeq1  3876  ifeq2  3877  pweq  3945  sneq  3969  csbsng  4021  csbprg  4022  rabsn  4030  preq1  4042  preq2  4043  tpeq1  4051  tpeq2  4052  tpeq3  4053  prprc1  4073  opeq1  4158  opeq2  4159  oteq1  4167  oteq2  4168  oteq3  4169  unieq  4198  csbuni  4218  inteq  4229  iineq1  4284  iineq2  4287  dfiin2g  4302  iinrab  4331  iinin1  4340  iinxprg  4350  iununi  4359  opabbid  4458  mpteq12f  4472  csbmpt12  4735  xpeq1  4853  xpeq2  4854  rneq  5066  reseq1  5105  reseq2  5106  resmpt  5160  imaeq1  5169  imaeq2  5170  mptcnv  5244  dmpropg  5316  rnpropg  5323  cores  5345  cores2  5355  xpco  5383  predeq123  5388  suceq  5495  iotaeq  5561  iotabi  5562  fntpg  5644  imain  5669  f1oprswap  5868  fveq1  5878  fveq2  5879  fvres  5893  csbfv12  5914  fnimapr  5944  fvco2  5955  residpr  6084  fsnunfv  6120  fsnunres  6121  funiunfv  6171  fliftf  6226  isoini2  6248  riotaeqdv  6271  riotabidv  6272  riotauni  6276  riotabidva  6286  snriota  6299  oveq  6314  oveq1  6315  oveq2  6316  oprabbid  6363  mpt2eq123  6369  mpt2eq123dva  6371  mpt2eq3dva  6374  resmpt2  6413  ovres  6455  f1ocnvd  6537  ofeq  6552  ofreq  6553  fpar  6919  wrecseq123  7047  onovuni  7079  recseq  7110  tfr2a  7131  rdgeq1  7147  rdgeq2  7148  rdgsucmptf  7164  frsucmpt  7173  seqomeq12  7189  seqomsuc  7192  omopthi  7376  eceq1  7417  eceq2  7419  qseq1  7431  qseq2  7432  uniqs  7441  ecinxp  7456  qsinxp  7457  erovlem  7477  ecopovtrn  7484  ixpeq1  7551  supeq1  7977  supeq2  7980  supeq3  7981  supeq123d  7982  infeq1  8010  infeq2  8013  infeq3  8014  infeq123d  8015  infiso  8041  oieq1  8045  oieq2  8046  ordtypelem1  8051  inf3lemc  8149  wemapwe  8220  r1sucg  8258  r1limg  8260  rankprb  8340  karden  8384  cardiun  8434  acneq  8492  alephlim  8516  alephsuc  8517  alephfplem2  8554  infpssrlem2  8752  fin23lem34  8794  fin23lem35  8795  zorn2lem1  8944  zorn2lem7  8950  fpwwe2lem6  9078  fpwwe2lem13  9085  addpiord  9327  mulpiord  9328  addpqnq  9381  mulpqnq  9384  addassnq  9401  mulassnq  9402  distrnq  9404  lterpq  9413  ltexnq  9418  ltsrpr  9519  00sr  9541  recexsrlem  9545  mulgt0sr  9547  addcnsrec  9585  mulcnsrec  9586  negeq  9887  csbnegg  9892  negsubdi  9950  mulneg1  10076  negfi  10576  deceq1  11077  deceq2  11078  xnegeq  11523  fseq1p1m1  11894  om2uzrdg  12208  uzrdgsuci  12212  seqeq1  12254  seqeq2  12255  seqeq3  12256  seqfeq4  12300  seqof  12308  hashprg  12610  hashmap  12648  hashtpg  12682  csbwrdg  12747  s1eq  12792  cats1co  13011  s2eqd  13018  s3eqd  13019  s4eqd  13020  s5eqd  13021  s6eqd  13022  s7eqd  13023  s8eqd  13024  xpcogend  13113  shftval  13214  limsupgle  13612  lo1eq  13709  rlimeq  13710  sumeq1  13832  sumeq2w  13835  sumeq2ii  13836  zsum  13861  sumss2  13869  fsumsplitsnun  13893  isumclim3  13897  fsumcom2  13912  incexclem  13971  incexc2  13973  isumshft  13974  prodeq1f  14039  prodeq2w  14043  prodeq2ii  14044  zprod  14068  fprodm1s  14101  fprodp1s  14102  fprodcom2  14115  iprodclim3  14130  ef0lem  14210  ruclem7  14365  sadcp1  14508  smupp1  14533  smueqlem  14543  algrp1  14612  dfphi2  14801  prmdiveq  14813  pceulem  14874  vdwlem6  15015  cshwsiun  15148  setsid  15242  elbasfv  15248  elbasov  15249  imastset  15501  imasvscaval  15522  xpscg  15542  isoval  15748  funcoppc  15858  fulloppc  15905  fuccofval  15942  natpropd  15959  catccofval  16073  xpchomfval  16142  xpccofval  16145  lubfval  16302  glbfval  16315  grpidpropd  16582  gsumpropd2lem  16594  frmdplusg  16716  grpinvpropd  16807  grpsubpropd  16834  grpsubpropd2  16835  mulgpropd  16869  oppgmnd  17083  symgplusg  17108  sylow1lem2  17329  sylow3lem1  17357  prds1  17920  pwsmgp  17924  opprring  17937  rngidpropd  18001  dvdsrpropd  18002  unitpropd  18003  invrpropd  18004  rhm1  18036  lmhmpropd  18374  lidlrsppropd  18531  lpival  18546  ressascl  18645  asclpropd  18647  aspval2  18648  psrbas  18679  psrplusg  18682  psrmulr  18685  psrvscafval  18691  resspsrbas  18716  ressmplbas2  18756  opsrle  18776  opsrbaslem  18778  vr1val  18862  ressply1add  18900  ressply1mul  18901  ressply1vsca  18902  psrplusgpropd  18906  mplbaspropd  18907  psropprmul  18908  ply1baspropd  18913  ply1plusgpropd  18914  ply1sca2  18924  subrgvr1  18931  coe1mul2lem2  18938  ply1coe1eq  18969  zrhpropd  19163  znle  19184  frlmplusgval  19403  frlmvscafval  19405  mamudi  19505  mamudir  19506  matrcl  19514  oftpos  19554  mattpos1  19558  mdetfval  19688  mdetrlin  19704  mdetrsca  19705  mdetrsca2  19706  mdetrlin2  19709  mdetunilem5  19718  madufval  19739  madugsum  19745  idmatidpmat  19838  cpmidpmat  19974  cncmp  20484  2ndcsep  20551  llyeq  20562  nllyeq  20563  xkouni  20691  hmphindis  20889  xkocnv  20906  ptcmplem2  21146  snclseqg  21208  prdstmdd  21216  ustexsym  21308  ucnextcn  21397  metreslem  21455  comet  21606  nrmmetd  21667  nmpropd  21686  isngp3  21690  ngpds  21695  subgnm  21719  tngnm  21737  idnghm  21842  cnmetdval  21869  cnmpt2pc  22034  htpyco2  22088  phtpyco2  22099  clsocv  22299  rrxprds  22426  rrxnm  22428  ovolunlem1a  22527  voliunlem3  22584  ioombl1lem4  22593  uniioombllem4  22623  itg11  22728  itgeq1f  22808  itgeq2  22814  iblss2  22842  itgss  22848  itgeqa  22850  itgfsum  22863  itgsplit  22872  ditgeq1  22882  ditgeq2  22883  ditgeq3  22884  dvcmulf  22978  dvmptfsum  23006  dvcnvrelem2  23049  mdegfval  23090  mdegpropd  23112  deg1propd  23114  plyeq0  23244  coe11  23286  dgrlt  23299  dgradd2  23301  dgrmulc  23304  dvply1  23316  fta1lem  23339  pserulm  23456  rlimcnp2  23971  jensenlem1  23991  basellem5  24090  dchrbas  24242  dchrrcl  24247  dchrplusg  24254  dchrfi  24262  lgsdi  24339  lgseisenlem2  24357  lgsquadlem3  24363  dchrmusumlema  24410  rpvmasum2  24429  dchrisum0lema  24431  pntlemg  24515  colperpexlem2  24852  axlowdimlem13  25063  nbgraf1olem5  25252  nb3graprlem1  25258  constr2spthlem1  25403  constr3pthlem1  25462  constr3pthlem2  25463  avril1  25979  0vfval  26306  imsval  26398  imsdval  26399  bcseqi  26854  normpythi  26876  cm0  27343  fh1  27352  pjcji  27418  opsqrlem5  27878  pjsdi2i  27891  pjclem3  27931  pjci  27934  golem1  28005  iunrdx  28256  ofresid  28319  mpteq12df  28332  resmptf  28333  f1od2  28384  gsumvsca1  28619  gsumvsca2  28620  rhmopp  28656  resv1r  28674  fzto1st1  28689  crefeq  28746  xrge0mulc1cn  28821  qqhval2  28860  esumeq12dvaf  28926  esumeq2  28931  esumf1o  28945  esumfzf  28964  esumss  28967  esumpfinvalf  28971  ofceq  28992  itgeq12dv  29232  ccatmulgnn0dir  29500  bnj956  29660  bnj1385  29716  bnj96  29748  bnj548  29780  bnj553  29781  bnj554  29782  bnj602  29798  bnj18eq1  29810  bnj1234  29894  bnj1296  29902  bnj1318  29906  bnj1442  29930  bnj1450  29931  cvmliftlem5  30084  cvmliftlem10  30089  cvmlift2lem9  30106  cvmliftphtlem  30112  mthmpps  30292  mpteq12d  30483  rdgprc  30512  dfrdg2  30513  trpredeq1  30532  trpredeq2  30533  trpredeq3  30534  wsuceq123  30568  wlimeq12  30573  altopthsn  30799  altxpeq1  30811  altxpeq2  30812  ee7.2aOLD  31192  bj-rabbida2  31588  bj-sngleq  31631  bj-tageq  31640  bj-projeq  31656  bj-projval  31660  bj-1upleq  31663  bj-pr1eq  31666  bj-pr2eq  31680  csbopg2  31795  csbpredg  31797  csbwrecsg  31798  csbrecsg  31799  csbrdgg  31800  csboprabg  31801  csbmpt22g  31802  finxpeq1  31848  finxpeq2  31849  csbfinxpg  31850  finxpreclem4  31856  finixpnum  31994  ptrest  32003  poimirlem3  32007  poimirlem9  32013  poimirlem15  32019  poimirlem16  32020  poimirlem26  32030  poimirlem27  32031  mbfposadd  32052  cnambfre  32053  iblabsnclem  32069  ftc1anclem1  32081  heiborlem4  32210  heiborlem6  32212  mpt2bi123f  32470  iineq12f  32472  mptbi12f  32474  riotaclbgBAD  32590  toycom  32610  ldualvbase  32763  ldualfvadd  32765  ldualsca  32769  ldualsbase  32770  ldualsaddN  32771  ldualfvs  32773  ldual0  32784  ldual1  32785  ldualneg  32786  cdleme19f  33946  cdleme20m  33961  cdleme21k  33976  cdleme27b  34006  cdleme31so  34017  cdleme31sn  34018  cdleme31se  34020  cdleme31se2  34021  cdleme31sc  34022  cdleme31sde  34023  cdleme31fv  34028  cdleme40v  34107  cdleme43dN  34130  cdlemeg46ngfr  34156  ltrnco4  34377  tgrpbase  34384  tgrpopr  34385  erngbase  34439  erngfplus  34440  erngfmul  34443  erngbase-rN  34447  erngfplus-rN  34448  erngfmul-rN  34451  dvasca  34644  dvavbase  34651  dvafvadd  34652  dvafvsca  34654  tendocnv  34660  dvhsca  34721  dvhfplusr  34723  dvhvbase  34726  dvhfvadd  34730  dvhfvsca  34739  lcdvadd  35236  lcdsbase  35239  lcdsadd  35240  lcdvs  35242  lcd0  35247  lcd1  35248  lcdneg  35249  imaiinfv  35606  mapfzcons1  35630  rexrabdioph  35708  dnnumch1  35973  dnwech  35977  aomclem6  35988  pwssplit4  36018  pwfi2f1o  36025  mendplusgfval  36122  mendvscafval  36127  uzmptshftfval  36765  dropab1  36870  dropab2  36871  csbunigOLD  37275  csbfv12gALTOLD  37276  csbxpgOLD  37277  csbresgOLD  37279  csbrngOLD  37280  csbima12gALTOLD  37281  itgsinexplem1  37927  wallispi2lem2  38046  fourierdlem36  38118  etransclem4  38215  afveq12d  38780  aoveq123d  38825  aovfundmoveq  38828  aovnuoveq  38838  aovvoveq  38839  aovovn0oveq  38841  resisresindm  39155  fsumsplitsndif  39242  uhgrvtxedgiedgb  39388  nb3grprlem1  39618  crctcshlem2  39996  rngccofvalALTV  40497  ringccofvalALTV  40560  rhmsubclem2  40597  rhmsubcALTVlem2  40616  xpprsng  40621  aacllem  41046
  Copyright terms: Public domain W3C validator