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

Theorem eqeq12d 2449
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12d.1  |-  ( ph  ->  A  =  B )
eqeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eqeq12d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 eqeq12 2447 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652
This theorem is referenced by:  cdeqeq  3148  sbceqg  3259  csbing  3540  csbifg  3759  uniprg  4022  unisng  4024  intprg  4076  iununi  4167  csbopabg  4275  limeq  4585  ordunisuc  4803  onsucuni2  4805  orduninsuc  4814  csbima12g  5204  dmsnsnsn  5339  cnvsng  5346  csbiotag  5438  csbfv12gALT  5730  fveqres  5755  fvmptf  5812  eqfnfv2f  5822  fvreseq  5824  fmptco  5892  fnressn  5909  fvsng  5918  fnpr  5941  fnprOLD  5942  fnsuppres  5943  cocan1  6015  cocan2  6016  fliftfun  6025  weniso  6066  csbovg  6103  eqfnov  6167  ovmpt2s  6188  ov2gf  6189  ovmpt2dxf  6190  caovcomg  6233  caovassg  6236  caovcang  6239  caovcanrd  6241  caovcan  6242  caovdig  6252  caovdirg  6255  caovmo  6275  grprinvlem  6276  grprinvd  6277  offveqb  6317  caofid0l  6323  caofid0r  6324  caofass  6329  caonncan  6333  op1stg  6350  op2ndg  6351  f1o2ndf1  6445  opabiota  6529  csbriotag  6553  onfununi  6594  tfrlem1  6627  tfrlem2  6628  tfrlem3  6629  tfrlem3a  6630  tfrlem9  6637  tfrlem11  6640  tfrlem12  6641  tfr3  6651  tz7.44-1  6655  tz7.44-2  6656  tz7.44-3  6657  rdglem1  6664  rdg0g  6676  seqomlem1  6698  abianfp  6707  oalim  6767  omlim  6768  oelim  6769  oa0r  6773  om0r  6774  om1r  6777  oaass  6795  oarec  6796  odi  6813  omass  6814  oelim2  6829  oeoalem  6830  oeoa  6831  oeoelem  6832  oeoe  6833  nna0r  6843  nnacom  6851  nnaass  6856  nndi  6857  nnmass  6858  nnmsucr  6859  nnmcom  6860  oaabs  6878  oaabs2  6879  omabs  6881  ecovcom  7006  ecovass  7007  ecovdi  7008  dom2lem  7138  unxpdomlem2  7305  unxpdomlem3  7306  ixpfi2  7396  fipreima  7403  ordiso2  7473  wemaplem1  7504  wemaplem2  7505  wemapso2lem  7508  cantnfval2  7613  cantnfp1lem3  7625  oemapvali  7629  cantnflem1c  7632  cantnflem1  7634  wemapwe  7643  tcvalg  7666  rankvalg  7732  rankonidlem  7743  ranklim  7759  rankuni  7778  cardprclem  7855  cardprc  7856  carduni  7857  fseqenlem1  7894  fodomacn  7926  alephcard  7940  alephfp2  7979  alephval3  7980  dfac12lem1  8012  dfac12lem2  8013  dfac12r  8015  ackbij1lem5  8093  ackbij1lem8  8096  ackbij1lem14  8102  ackbij1lem16  8104  ackbij2lem3  8110  cardcf  8121  sornom  8146  fin23lem28  8209  isf32lem2  8223  itunitc  8290  ituniiun  8291  axdc3lem2  8320  axdc4lem  8324  ttukeylem3  8380  ttukey2g  8385  fpwwe2lem8  8501  fpwwecbv  8508  canth4  8511  pwfseqlem2  8523  addcanpi  8765  mulcanpi  8766  recrecnq  8833  ltexnq  8841  genpv  8865  0idsr  8961  1idsr  8962  ax1rid  9025  mulid1  9077  addcan  9239  addcan2  9240  mulcand  9644  mulcan2d  9645  div11  9693  divmuleq  9708  conjmul  9720  eqneg  9723  ofsubeq0  9986  rpnnen1  10594  cnref1o  10596  xmulasslem  10853  xmulass  10855  xadddi2  10865  prunioo  11014  fzsuc2  11093  fzprval  11095  fztpval  11096  modadd1  11266  modmul1  11267  om2uzsuci  11276  om2uzrdg  11284  uzrdgxfr  11294  seq1  11324  seqp1  11326  seqfveq2  11333  seqfveq  11335  seqshft2  11337  seqsplit  11344  seqcaopr3  11346  seqcaopr2  11347  seqf1olem2a  11349  seqf1olem2  11351  seqf1o  11352  seqid  11356  seqid2  11357  seqhomo  11358  ser1const  11367  seqof2  11369  mulexp  11407  expadd  11410  expmul  11413  binom2  11484  sq01  11489  modexp  11502  bcpasc  11600  hashgadd  11639  hashdom  11641  hashfzo  11682  hashxplem  11684  hashxp  11685  hashmap  11686  hashpw  11687  hashbclem  11689  hashbc  11690  hashfacen  11691  hashf1lem1  11692  hashf1lem2  11693  hashf1  11694  seqcoll  11700  ccatopth  11764  ccatopth2  11765  cats1un  11778  replim  11909  cjreb  11916  cjexp  11943  absexp  12097  abs1m  12127  recan  12128  isercoll2  12450  iseraltlem2  12464  iseraltlem3  12465  sumeq2w  12474  sumeq2ii  12475  zsum  12500  fsum  12502  fsumf1o  12505  sumss  12506  fsumcvg2  12509  fsumadd  12520  isummulc2  12534  fsum2d  12543  fsummulc2  12555  fsumconst  12561  fsumparts  12573  fsumrelem  12574  fsumiun  12588  binom  12597  bcxmas  12603  incexclem  12604  isumshft  12607  isumnn0nn  12610  climcndslem1  12617  climcndslem2  12618  mertenslem2  12650  efne0  12686  efexp  12690  demoivreALT  12790  moddvds  12847  bitsinv1  12942  sadadd2  12960  smu01lem  12985  smupval  12988  smueqlem  12990  smumullem  12992  gcdaddm  13017  bezoutlem1  13026  bezout  13030  gcddiv  13037  seq1st  13050  alginv  13054  algfx  13059  isprm2lem  13074  nn0gcdsq  13132  crt  13155  eulerthlem2  13159  pythagtriplem1  13178  iserodd  13197  pcqmul  13215  pcexp  13221  pcneg  13235  pcmpt  13249  pcfac  13256  prmreclem2  13273  prmreclem3  13274  1arith  13283  vdwpc  13336  ramcl  13385  imasval  13725  ercpbllem  13761  xpscfv  13775  iscat  13885  iscatd  13886  catideu  13888  iscatd2  13894  catlid  13896  catrid  13897  catass  13899  proplem  13903  homfeq  13908  comfeq  13920  catpropd  13923  moni  13950  epii  13957  sectffval  13964  sectfval  13965  oppcsect  13987  sectmon  13991  isfunc  14049  funcid  14055  funcco  14056  funcpropd  14085  isfull  14095  fthsect  14110  fthmon  14112  natfval  14131  isnat  14132  nati  14140  fucsect  14157  natpropd  14161  setcmon  14230  setcepi  14231  setcsect  14232  evlfcl  14307  uncfcurf  14324  yoniso  14370  isacs5lem  14583  acsdrscl  14584  acsficl  14585  latdisdlem  14603  latdisd  14604  isdlat  14607  dlatmjdi  14608  isps  14622  ismnd  14680  mgmidmo  14681  mndlem1  14682  mgmlrid  14700  ismndd  14707  mndpropd  14709  imasmnd2  14720  ismhm  14728  mhmpropd  14732  mhmlin  14733  mhmeql  14752  gsumvalx  14762  gsumval2  14771  gsumccat  14775  gsumwmhm  14778  frmdgsum  14795  isgrp  14804  grppropd  14811  isgrpd2e  14815  isgrpid2  14829  grpidd2  14830  grpinvfval  14831  grpinvpropd  14854  grpsubrcan  14858  grplactcnv  14875  mulgnn0p1  14889  mulgneg2  14905  mulgnnass  14906  mulgnn0ass  14907  mulgass  14908  mhmmulg  14910  imasgrp2  14921  isghm  14994  ghmlin  14999  ghmeql  15016  isga  15056  gagrpid  15059  gaass  15062  galcan  15069  orbsta  15078  cayleylem2  15099  cntzfval  15107  elcntz  15109  cntzsnval  15111  elcntzsn  15112  cntzi  15116  resscntz  15118  cntzmhm  15125  gsumwrev  15150  odfval  15159  mndodcong  15168  odbezout  15182  odeq1  15184  submod  15191  gexval  15200  gexdvds  15206  ispgp  15214  sylow1lem1  15220  sylow2alem1  15239  sylow2alem2  15240  sylow2blem2  15243  efgmnvl  15334  efgredlemc  15365  efgredeu  15372  frgpuptinv  15391  frgpup1  15395  frgpup3lem  15397  iscmn  15407  cmnpropd  15409  iscmnd  15412  abladdsub4  15426  submcmn2  15446  divsabl  15468  iscyg  15477  cygabl  15488  gsum2d  15534  dmdprd  15547  dprdval  15549  dprdfcntz  15561  subgdmdprd  15580  dprd2da  15588  dpjrid  15608  pgpfac1lem3a  15622  ablfaclem3  15633  ablfac2  15635  isrng  15656  rngpropd  15683  mulgass2  15698  imasrng  15713  dvdsr  15739  dvreq1  15786  isdrng  15827  drngprop  15834  isdrngd  15848  drngpropd  15850  isabv  15895  abvmul  15905  issrng  15926  issrngd  15937  islmod  15942  lmodlema  15943  islmodd  15944  lmodprop2d  15994  islmhm  16091  lmhmlin  16099  islmhm2  16102  lmhmeql  16119  lmhmpropd  16133  islbs  16136  lbspropd  16159  divscrng  16299  islpir  16308  rrgval  16335  unitrrg  16341  isassa  16363  assalem  16364  isassad  16370  assapropd  16374  mvrf1  16477  mplmonmul  16515  mplcoe1  16516  mplcoe3  16517  mplcoe2  16518  coe1tm  16653  ply1sclf1  16668  cnfldmulg  16721  cnfldexp  16722  prmirredlem  16761  chrcong  16798  zndvds  16818  znf1o  16820  znunit  16832  cygznlem3  16838  frgpcyg  16842  isphl  16847  ipcj  16853  iporthcom  16854  ip2eq  16872  isphld  16873  phlpropd  16874  ocvfval  16881  iscss  16898  ishil  16933  isobs  16935  obsip  16936  obslbs  16945  isperf  17203  restperf  17236  cmpsub  17451  iscon  17464  2ndcsep  17510  elptr2  17594  ptbasin  17597  dfac14  17638  txcnp  17640  ptcnplem  17641  ptcnp  17642  cnmpt11  17683  cnmpt21  17691  cnmptcom  17698  kqfeq  17744  isr0  17757  pt1hmeo  17826  ustexsym  18233  isusp  18279  imasdsf1olem  18391  isxms  18465  xmspropd  18491  imasf1oxms  18507  stdbdmopn  18536  isngp3  18633  ngppropd  18666  isnlm  18699  nmvs  18700  xrsxmet  18828  cnheibor  18968  htpyi  18987  htpycc  18993  pi1xfr  19068  pi1coghm  19074  isclm  19077  lmhmclm  19099  clmmulg  19106  iscph  19121  tchcph  19182  cmetcaulem  19229  bcth3  19272  ovolunlem1a  19380  ovolicc2lem1  19401  ovolicc2lem4  19404  ovolicc2  19406  mblsplit  19416  volun  19427  volfiniun  19429  voliunlem1  19432  volsup  19438  ioorinv  19456  uniioombllem2  19463  vitalilem3  19490  mbfeqalem  19522  mbflim  19548  itgeqa  19693  itgconst  19698  itgfsum  19706  itgsplitioo  19717  dvnadd  19803  dvnres  19805  dvexp  19827  dvmptfsum  19847  mvth  19864  dvlip  19865  lhop1lem  19885  dvcvx  19892  evlslem1  19924  mpfrcl  19927  evlsval  19928  mdegle0  19988  ply1nzb  20033  mon1pval  20052  facth1  20075  ig1pval  20083  dgrmulc  20177  dgrcolem1  20179  dgrcolem2  20180  dgrco  20181  coecj  20184  vieta1lem2  20216  vieta1  20217  elqaalem3  20226  dvntaylp  20275  ulmss  20301  mtest  20308  sineq0  20417  efif1olem4  20435  cxpexp  20547  mulcxplem  20563  mulcxp  20564  cxpmul2  20568  cxpeq  20629  affineequiv2  20656  quad2  20667  dcubic  20674  leibpi  20770  o1cxp  20801  scvxcvx  20812  wilthlem1  20839  wilthlem2  20840  perfect  21003  dchrelbas2  21009  dchrinv  21033  dchrptlem2  21037  lgsne0  21105  lgsqrlem2  21114  lgsdchr  21120  lgseisenlem2  21122  lgsquad2lem2  21131  dchrisumlem1  21171  qabvexp  21308  ostthlem1  21309  ostthlem2  21310  ostth3  21320  usgraidx2v  21400  nbgraf1olem5  21443  cusgrasize  21475  wlkntrllem2  21548  2wlklem  21552  constr1trl  21576  redwlk  21594  wlkdvspthlem  21595  iscrct  21599  iscycl  21600  fargshiftf1  21612  fargshiftfva  21614  usgrcyclnl2  21616  3v3e3cycl1  21619  constr3trllem5  21629  4cycl4v4e  21641  4cycl4dv4e  21643  iseupa  21675  eupatrl  21678  eupaseg  21683  eupap1  21686  eupath2  21690  isgrpo  21772  grpoass  21779  grpoidinvlem3  21782  grpoidinv  21784  grpoideu  21785  grpoidinv2  21794  grpoinvfval  21800  isgrp2d  21811  gxcom  21845  gxinv  21846  gxnn0add  21850  gxnn0mul  21853  isablo  21859  ablocom  21861  gxdi  21872  issubgoilem  21885  isass  21892  opidon  21898  exidu1  21902  cmpidelt  21905  elghomlem2  21938  ghomlin  21940  ghgrplem2  21943  ghgrp  21944  ghablo  21945  isrngo  21954  rngoid  21959  rngoideu  21960  rngodi  21961  rngodir  21962  rngoass  21963  iscom2  21988  vci  22015  vcid  22018  vcdi  22019  vcdir  22020  vcass  22021  isvclem  22044  isnvlem  22077  nvmeq0  22133  nvs  22139  imsmetlem  22170  islno  22242  lnolin  22243  ishmo  22300  isphg  22306  phpar2  22312  phpar  22313  ipdiri  22319  ipasslem1  22320  ipasslem5  22324  ipasslem11  22329  ipassi  22330  dipdir  22331  dipass  22334  ip2eqi  22346  htth  22409  hvsubsub4  22550  hvnegdi  22557  hvaddcan  22560  hvaddcan2  22561  hvsubcan  22564  hvsubcan2  22565  hvaddsub4  22568  hial2eq  22596  normlem9at  22611  normsq  22624  norm-iii  22630  normsub  22633  normpyth  22635  normpar  22645  polid  22649  ococ  22896  chj0  22987  chlejb1  23002  chdmm1  23015  chjass  23023  spanun  23035  spansn  23049  elspansn2  23057  cmbr  23074  cmbr3  23098  pjoml2  23101  pjoml3  23102  osum  23135  spansnj  23137  pjch1  23160  pjadji  23175  pjaddi  23176  pjinormi  23177  pjsubi  23178  pjmuli  23179  pjcjt2  23182  pjch  23184  pjopyth  23210  pjpyth  23215  hoaddcom  23265  hoaddass  23273  hocsubdir  23276  hoaddid1  23282  ho0sub  23288  honegsub  23290  adjsym  23324  eigrei  23325  eigre  23326  eigposi  23327  eigorth  23329  ellnop  23349  elhmop  23364  ellnfn  23374  cnvadj  23383  lnopl  23405  unop  23406  hmop  23413  lnfnl  23422  adj1  23424  eleigvec  23448  hoddi  23481  lnopeq0lem2  23497  lnopunilem1  23501  lnopunilem2  23502  lnopunii  23503  elunop2  23504  lnophmi  23509  lnfnmul  23539  cnlnadjlem5  23562  branmfn  23596  bra11  23599  hmopidmchi  23642  hmopidmch  23644  hmopidmpj  23645  pjss2coi  23655  pjssmi  23656  pjssge0i  23657  pjidmco  23672  dfpjop  23673  elpjrn  23681  isst  23704  ishst  23705  hstel2  23710  stj  23726  mdbr  23785  mdi  23786  mdbr3  23788  dmdbr  23790  dmdmd  23791  dmdi  23793  dmdbr3  23796  mddmd2  23800  mdsl1i  23812  chjatom  23848  iuninc  23999  fmptcof2  24064  bcm1n  24139  xmulcand  24155  xrsmulgzz  24188  pstmxmet  24280  cnre2csqlem  24296  mndpluscn  24300  qqhval2  24354  esumfzf  24447  esumcvg  24464  ofcfeqd2  24472  ismeas  24541  isrnmeas  24542  measvun  24551  probun  24665  facgam  24838  subfacp1lem3  24856  subfacp1lem4  24857  subfacp1lem5  24858  subfacp1lem6  24859  subfacval2  24861  erdszelem9  24873  sconpht  24904  ptpcon  24908  cvmliftmolem1  24956  cvmliftmolem2  24957  cvmliftlem10  24969  cvmlift2  24991  cvmliftphtlem  24992  ghomgrpilem1  25084  relexpsucr  25118  relexpsucl  25120  relexpcnv  25121  relexpadd  25126  sqdivzi  25172  mulcan2g  25178  shftvalg  25196  clim2prod  25205  prodfrec  25212  prodeq2w  25227  prodeq2ii  25228  zprod  25252  fprod  25256  fprodf1o  25261  fprodser  25264  fprodmul  25273  fproddiv  25274  prodsn  25275  fprodabs  25286  fprodefsum  25287  fprodconst  25291  fprod2d  25294  iprodefisumlem  25306  binomfallfac  25346  faclimlem1  25351  fprb  25384  rdgprc  25406  dfrdg2  25407  preddowncl  25451  poseq  25508  soseq  25509  wfr3g  25510  wfrlem1  25511  wfrlem12  25522  wfrlem14  25524  wfrlem15  25525  wfr2  25528  wfr2c  25529  tfr3ALT  25534  frr3g  25535  frrlem1  25536  frrlem11  25548  sltval2  25565  sltres  25573  nofulllem5  25615  fvsingle  25715  fullfunfv  25742  brcgr  25787  brbtwn2  25792  colinearalglem1  25793  colinearalg  25797  ax5seglem1  25815  ax5seglem2  25816  ax5seglem8  25823  ax5seglem9  25824  axlowdimlem13  25841  axlowdimlem16  25844  axlowdim1  25846  axcontlem1  25851  axcontlem2  25852  axcontlem6  25856  axcontlem7  25857  axcontlem8  25858  lineelsb2  26030  bpolyval  26043  bpolydif  26049  rankung  26055  ranksng  26056  rankpwg  26058  voliunnfl  26196  volsupnfl  26197  opnregcld  26270  cldregopn  26271  neibastop3  26328  cocanfo  26356  upixp  26368  sdclem2  26383  caushft  26404  ismtycnv  26448  ismtyima  26449  ismtybndlem  26452  ismtyres  26454  bfplem2  26469  bfp  26470  grpoeqdivid  26493  ghomco  26495  rngohomval  26517  isrngohom  26518  rngohomadd  26522  rngohommul  26523  iscringd  26546  crngocom  26548  crngohomfo  26553  dmncan2  26624  fnelfp  26673  ismrcd2  26690  ismrc  26692  dvdsrabdioph  26807  fphpdo  26815  rmxypairf1o  26911  monotoddzzfi  26942  monotoddzz  26943  oddcomabszz  26944  rmxdioph  27024  expdiophlem2  27030  dnnumch3  27059  aomclem8  27074  islssfg  27083  unxpwdom3  27171  gicabl  27178  pmtrfrn  27315  cntzsdrg  27425  idomodle  27427  fgraphxp  27445  hausgraph  27446  caofcan  27455  expgrowth  27467  fmuldfeq  27627  climmulf  27644  climexp  27645  climsuse  27648  climrecf  27649  stoweidlem30  27693  stoweidlem48  27711  wallispilem4  27731  wallispi2lem1  27734  wallispi2lem2  27735  csbafv12g  27915  csbaovg  27958  swrdccatin1  28091  swrdccatin12c  28103  swrdccat3b  28106  usgra2pthspth  28179  usgra2wlkspthlem1  28180  usgra2pthlem1  28184  usgra2pth  28185  2pthfrgra  28259  bnj1385  29058  bnj66  29085  bnj106  29093  bnj155  29104  bnj222  29108  bnj540  29117  bnj591  29136  bnj594  29137  bnj611  29143  bnj893  29153  bnj1000  29166  bnj966  29169  bnj1112  29206  bnj1234  29236  bnj1253  29240  bnj1280  29243  bnj1326  29249  bnj1450  29273  bnj1463  29278  bnj1529  29293  lshpset  29615  lcvexchlem4  29674  lcvexchlem5  29675  lflset  29696  islfl  29697  lfli  29698  islfld  29699  eqlkr3  29738  isopos  29817  oposlem  29820  opcon3b  29833  cmtvalN  29848  omllaw  29880  cvlexchb2  29968  cvlatexchb2  29972  cvlsupr2  29980  4atlem9  30239  4atlem10a  30240  4atlem11a  30243  4atlem12a  30246  4at2  30250  pmapglb2N  30407  pmapglb2xN  30408  paddasslem17  30472  ispsubclN  30573  ispsubcl2N  30583  lhpmod2i2  30674  lhpmod6i1  30675  4atexlemex2  30707  4atex  30712  4atex2-0aOLDN  30714  4atex2-0cOLDN  30716  ldilval  30749  ltrnfset  30753  ltrnset  30754  isltrn  30755  ltrneq2  30784  trnfsetN  30791  trnsetN  30792  istrnN  30793  cdlemd5  30838  cdleme0moN  30861  cdleme0nex  30926  cdleme18d  30931  cdleme31so  31015  cdleme31fv  31026  cdlemg2jlemOLDN  31229  cdlemg2fvlem  31230  cdlemg2klem  31231  istendo  31396  tendovalco  31401  tendoeq2  31410  dicelvalN  31815  dihval  31869  dihcnv11  31912  dihmeetlem13N  31956  dihlspsnat  31970  dochn0nv  32012  dochkrshp4  32026  lpolsetN  32119  lpolsatN  32125  lpolpolsatN  32126  lcfl1lem  32128  lclkrlem2a  32144  lclkrlem2e  32148  lcfls1lem  32171  lclkrs2  32177  lcdfval  32225  lcdval  32226  mapdffval  32263  mapdfval  32264  mapd0  32302  mapdpglem30  32339  mapdhval  32361  mapdheq2  32366  hdmap1vallem  32435  hdmap1val  32436  hdmap1cbv  32440  hdmapval3N  32478  hdmap10  32480  hdmapeq0  32484  hdmap14lem12  32519  hdmap14lem13  32520  hgmapfval  32526  hgmapvs  32531  hgmapvv  32566  hlhilocv  32597
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-an 361  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator