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

Theorem eqeq12d 2299
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 2297 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1625
This theorem is referenced by:  cdeqeq  2988  sbceqg  3099  csbing  3378  csbifg  3595  uniprg  3844  unisng  3846  intprg  3898  iununi  3988  csbopabg  4096  limeq  4406  ordunisuc  4625  onsucuni2  4627  orduninsuc  4636  csbima12g  5024  dmsnsnsn  5153  cnvsng  5160  csbiotag  5250  csbfv12gALT  5538  fveqres  5562  fvmptf  5618  eqfnfv2f  5628  fvreseq  5630  fmptco  5693  fnressn  5707  fvsng  5716  fnsuppres  5734  cocan1  5803  cocan2  5804  fliftfun  5813  weniso  5854  csbovg  5891  eqfnov  5952  ovmpt2s  5973  ov2gf  5974  ovmpt2dxf  5975  caovcomg  6017  caovassg  6020  caovcang  6023  caovcanrd  6025  caovcan  6026  caovdig  6036  caovdirg  6039  caovmo  6059  grprinvlem  6060  grprinvd  6061  offveqb  6101  caofid0l  6107  caofid0r  6108  caofass  6113  caonncan  6117  op1stg  6134  op2ndg  6135  opabiota  6295  csbriotag  6319  onfununi  6360  tfrlem1  6393  tfrlem2  6394  tfrlem3  6395  tfrlem3a  6396  tfrlem9  6403  tfrlem11  6406  tfrlem12  6407  tfr3  6417  tz7.44-1  6421  tz7.44-2  6422  tz7.44-3  6423  rdglem1  6430  rdg0g  6442  seqomlem1  6464  abianfp  6473  oalim  6533  omlim  6534  oelim  6535  oa0r  6539  om0r  6540  om1r  6543  oaass  6561  oarec  6562  odi  6579  omass  6580  oelim2  6595  oeoalem  6596  oeoa  6597  oeoelem  6598  oeoe  6599  nna0r  6609  nnacom  6617  nnaass  6622  nndi  6623  nnmass  6624  nnmsucr  6625  nnmcom  6626  oaabs  6644  oaabs2  6645  omabs  6647  ecovcom  6771  ecovass  6772  ecovdi  6773  dom2lem  6903  unxpdomlem2  7070  unxpdomlem3  7071  ixpfi2  7156  fipreima  7163  ordiso2  7232  wemaplem1  7263  wemaplem2  7264  wemapso2lem  7267  cantnfval2  7372  cantnfp1lem3  7384  oemapvali  7388  cantnflem1c  7391  cantnflem1  7393  wemapwe  7402  tcvalg  7425  rankvalg  7491  rankonidlem  7502  ranklim  7518  rankuni  7537  cardprclem  7614  cardprc  7615  carduni  7616  fseqenlem1  7653  fodomacn  7685  alephcard  7699  alephfp2  7738  alephval3  7739  dfac12lem1  7771  dfac12lem2  7772  dfac12r  7774  ackbij1lem5  7852  ackbij1lem8  7855  ackbij1lem14  7861  ackbij1lem16  7863  ackbij2lem3  7869  cardcf  7880  sornom  7905  fin23lem28  7968  isf32lem2  7982  itunitc  8049  ituniiun  8050  axdc3lem2  8079  axdc4lem  8083  ttukeylem3  8140  ttukey2g  8145  fpwwe2lem8  8261  fpwwecbv  8268  canth4  8271  pwfseqlem2  8283  addcanpi  8525  mulcanpi  8526  recrecnq  8593  ltexnq  8601  genpv  8625  0idsr  8721  1idsr  8722  ax1rid  8785  mulid1  8837  addcan  8998  addcan2  8999  mulcand  9403  mulcan2d  9404  div11  9452  divmuleq  9467  conjmul  9479  eqneg  9482  ofsubeq0  9745  rpnnen1  10349  cnref1o  10351  xmulasslem  10607  xmulass  10609  xadddi2  10619  prunioo  10766  fzsuc2  10844  fzprval  10846  fztpval  10847  modadd1  11003  modmul1  11004  om2uzsuci  11013  om2uzrdg  11021  uzrdgxfr  11031  seq1  11061  seqp1  11063  seqfveq2  11070  seqfveq  11072  seqshft2  11074  seqsplit  11081  seqcaopr3  11083  seqcaopr2  11084  seqf1olem2a  11086  seqf1olem2  11088  seqf1o  11089  seqid  11093  seqid2  11094  seqhomo  11095  ser1const  11104  mulexp  11143  expadd  11146  expmul  11149  binom2  11220  sq01  11225  modexp  11238  bcpasc  11335  hashgadd  11361  hashdom  11363  hashfzo  11385  hashxplem  11387  hashxp  11388  hashmap  11389  hashpw  11390  hashbclem  11392  hashbc  11393  hashfacen  11394  hashf1lem1  11395  hashf1lem2  11396  hashf1  11397  seqcoll  11403  ccatopth  11464  ccatopth2  11465  cats1un  11478  replim  11603  cjreb  11610  cjexp  11637  absexp  11791  abs1m  11821  recan  11822  isercoll2  12144  iseraltlem2  12157  iseraltlem3  12158  sumeq2w  12167  sumeq2ii  12168  zsum  12193  fsum  12195  fsumf1o  12198  sumss  12199  fsumcvg2  12202  fsumadd  12213  isummulc2  12227  fsum2d  12236  fsummulc2  12248  fsumconst  12254  fsumparts  12266  fsumrelem  12267  fsumiun  12281  binom  12290  bcxmas  12296  incexclem  12297  isumshft  12300  isumnn0nn  12303  climcndslem1  12310  climcndslem2  12311  mertenslem2  12343  efne0  12379  efexp  12383  demoivreALT  12483  moddvds  12540  bitsinv1  12635  sadadd2  12653  smu01lem  12678  smupval  12681  smueqlem  12683  smumullem  12685  gcdaddm  12710  bezoutlem1  12719  bezout  12723  gcddiv  12730  seq1st  12743  alginv  12747  algfx  12752  isprm2lem  12767  nn0gcdsq  12825  crt  12848  eulerthlem2  12852  pythagtriplem1  12871  iserodd  12890  pcqmul  12908  pcexp  12914  pcneg  12928  pcmpt  12942  pcfac  12949  prmreclem2  12966  prmreclem3  12967  1arith  12976  vdwpc  13029  ramcl  13078  imasval  13416  ercpbllem  13452  xpscfv  13466  iscat  13576  iscatd  13577  catideu  13579  iscatd2  13585  catlid  13587  catrid  13588  catass  13590  proplem  13594  homfeq  13599  comfeq  13611  catpropd  13614  moni  13641  epii  13648  sectffval  13655  sectfval  13656  oppcsect  13678  sectmon  13682  isfunc  13740  funcid  13746  funcco  13747  funcpropd  13776  isfull  13786  fthsect  13801  fthmon  13803  natfval  13822  isnat  13823  nati  13831  fucsect  13848  natpropd  13852  setcmon  13921  setcepi  13922  setcsect  13923  evlfcl  13998  uncfcurf  14015  yoniso  14061  isacs5lem  14274  acsdrscl  14275  acsficl  14276  latdisdlem  14294  latdisd  14295  isdlat  14298  dlatmjdi  14299  isps  14313  ismnd  14371  mgmidmo  14372  mndlem1  14373  mgmlrid  14391  ismndd  14398  mndpropd  14400  imasmnd2  14411  ismhm  14419  mhmpropd  14423  mhmlin  14424  mhmeql  14443  gsumvalx  14453  gsumval2  14462  gsumccat  14466  gsumwmhm  14469  frmdgsum  14486  isgrp  14495  grppropd  14502  isgrpd2e  14506  isgrpid2  14520  grpidd2  14521  grpinvfval  14522  grpinvpropd  14545  grpsubrcan  14549  grplactcnv  14566  mulgnn0p1  14580  mulgneg2  14596  mulgnnass  14597  mulgnn0ass  14598  mulgass  14599  mhmmulg  14601  imasgrp2  14612  isghm  14685  ghmlin  14690  ghmeql  14707  isga  14747  gagrpid  14750  gaass  14753  galcan  14760  orbsta  14769  cayleylem2  14790  cntzfval  14798  elcntz  14800  cntzsnval  14802  elcntzsn  14803  cntzi  14807  resscntz  14809  cntzmhm  14816  gsumwrev  14841  odfval  14850  mndodcong  14859  odbezout  14873  odeq1  14875  submod  14882  gexval  14891  gexdvds  14897  ispgp  14905  sylow1lem1  14911  sylow2alem1  14930  sylow2alem2  14931  sylow2blem2  14934  efgmnvl  15025  efgredlemc  15056  efgredeu  15063  frgpuptinv  15082  frgpup1  15086  frgpup3lem  15088  iscmn  15098  cmnpropd  15100  iscmnd  15103  abladdsub4  15117  submcmn2  15137  divsabl  15159  iscyg  15168  cygabl  15179  gsum2d  15225  dmdprd  15238  dprdval  15240  dprdfcntz  15252  subgdmdprd  15271  dprd2da  15279  dpjrid  15299  pgpfac1lem3a  15313  ablfaclem3  15324  ablfac2  15326  isrng  15347  rngpropd  15374  mulgass2  15389  imasrng  15404  dvdsr  15430  dvreq1  15477  isdrng  15518  drngprop  15525  isdrngd  15539  drngpropd  15541  isabv  15586  abvmul  15596  issrng  15617  issrngd  15628  islmod  15633  lmodlema  15634  islmodd  15635  lmodprop2d  15689  islmhm  15786  lmhmlin  15794  islmhm2  15797  lmhmeql  15814  lmhmpropd  15828  islbs  15831  lbspropd  15854  divscrng  15994  islpir  16003  rrgval  16030  unitrrg  16036  isassa  16058  assalem  16059  isassad  16065  assapropd  16069  mvrf1  16172  mplmonmul  16210  mplcoe1  16211  mplcoe3  16212  mplcoe2  16213  coe1tm  16351  ply1sclf1  16366  cnfldmulg  16408  cnfldexp  16409  prmirredlem  16448  chrcong  16485  zndvds  16505  znf1o  16507  znunit  16519  cygznlem3  16525  frgpcyg  16529  isphl  16534  ipcj  16540  iporthcom  16541  ip2eq  16559  isphld  16560  phlpropd  16561  ocvfval  16568  iscss  16585  ishil  16620  isobs  16622  obsip  16623  obslbs  16632  isperf  16884  restperf  16916  cmpsub  17129  iscon  17141  2ndcsep  17187  elptr2  17271  ptbasin  17274  dfac14  17314  txcnp  17316  ptcnplem  17317  ptcnp  17318  cnmpt11  17359  cnmpt21  17367  cnmptcom  17374  kqfeq  17417  isr0  17430  pt1hmeo  17499  imasdsf1olem  17939  isxms  17995  xmspropd  18021  imasf1oxms  18037  stdbdmopn  18066  isngp3  18122  ngppropd  18155  isnlm  18188  nmvs  18189  xrsxmet  18317  cnheibor  18455  htpyi  18474  htpycc  18480  pi1xfr  18555  pi1coghm  18561  isclm  18564  lmhmclm  18586  clmmulg  18593  iscph  18608  tchcph  18669  cmetcaulem  18716  bcth3  18755  ovolunlem1a  18857  ovolicc2lem1  18878  ovolicc2lem4  18881  ovolicc2  18883  mblsplit  18893  volun  18904  volfiniun  18906  voliunlem1  18909  volsup  18915  ioorinv  18933  uniioombllem2  18940  vitalilem3  18967  mbfeqalem  18999  mbflim  19025  itgeqa  19170  itgconst  19175  itgfsum  19183  itgsplitioo  19194  dvnadd  19280  dvnres  19282  dvexp  19304  dvmptfsum  19324  mvth  19341  dvlip  19342  lhop1lem  19362  dvcvx  19369  evlslem1  19401  mpfrcl  19404  evlsval  19405  mdegle0  19465  ply1nzb  19510  mon1pval  19529  facth1  19552  ig1pval  19560  dgrmulc  19654  dgrcolem1  19656  dgrcolem2  19657  dgrco  19658  coecj  19661  vieta1lem2  19693  vieta1  19694  elqaalem3  19703  dvntaylp  19752  ulmss  19776  mtest  19783  sineq0  19891  efif1olem4  19909  cxpexp  20017  mulcxplem  20033  mulcxp  20034  cxpmul2  20038  cxpeq  20099  affineequiv2  20126  quad2  20137  dcubic  20144  leibpi  20240  o1cxp  20271  scvxcvx  20282  wilthlem1  20308  wilthlem2  20309  perfect  20472  dchrelbas2  20478  dchrinv  20502  dchrptlem2  20506  lgsne0  20574  lgsqrlem2  20583  lgsdchr  20589  lgseisenlem2  20591  lgsquad2lem2  20600  dchrisumlem1  20640  qabvexp  20777  ostthlem1  20778  ostthlem2  20779  ostth3  20789  isgrpo  20865  grpoass  20872  grpoidinvlem3  20875  grpoidinv  20877  grpoideu  20878  grpoidinv2  20887  grpoinvfval  20893  isgrp2d  20904  gxcom  20938  gxinv  20939  gxnn0add  20943  gxnn0mul  20946  isablo  20952  ablocom  20954  gxdi  20965  issubgoilem  20978  isass  20985  opidon  20991  exidu1  20995  cmpidelt  20998  elghomlem2  21031  ghomlin  21033  ghgrplem2  21036  ghgrp  21037  ghablo  21038  isrngo  21047  rngoid  21052  rngoideu  21053  rngodi  21054  rngodir  21055  rngoass  21056  iscom2  21081  vci  21106  vcid  21109  vcdi  21110  vcdir  21111  vcass  21112  isvclem  21135  isnvlem  21168  nvmeq0  21224  nvs  21230  imsmetlem  21261  islno  21333  lnolin  21334  ishmo  21391  isphg  21397  phpar2  21403  phpar  21404  ipdiri  21410  ipasslem1  21411  ipasslem5  21415  ipasslem11  21420  ipassi  21421  dipdir  21422  dipass  21425  ip2eqi  21437  htth  21500  hvsubsub4  21641  hvnegdi  21648  hvaddcan  21651  hvaddcan2  21652  hvsubcan  21655  hvsubcan2  21656  hvaddsub4  21659  hial2eq  21687  normlem9at  21702  normsq  21715  norm-iii  21721  normsub  21724  normpyth  21726  normpar  21736  polid  21740  ococ  21987  chj0  22078  chlejb1  22093  chdmm1  22106  chjass  22114  spanun  22126  spansn  22140  elspansn2  22148  cmbr  22165  cmbr3  22189  pjoml2  22192  pjoml3  22193  osum  22226  spansnj  22228  pjch1  22251  pjadji  22266  pjaddi  22267  pjinormi  22268  pjsubi  22269  pjmuli  22270  pjcjt2  22273  pjch  22275  pjopyth  22301  pjpyth  22306  hoaddcom  22356  hoaddass  22364  hocsubdir  22367  hoaddid1  22373  ho0sub  22379  honegsub  22381  adjsym  22415  eigrei  22416  eigre  22417  eigposi  22418  eigorth  22420  ellnop  22440  elhmop  22455  ellnfn  22465  cnvadj  22474  lnopl  22496  unop  22497  hmop  22504  lnfnl  22513  adj1  22515  eleigvec  22539  hoddi  22572  lnopeq0lem2  22588  lnopunilem1  22592  lnopunilem2  22593  lnopunii  22594  elunop2  22595  lnophmi  22600  lnfnmul  22630  cnlnadjlem5  22653  branmfn  22687  bra11  22690  hmopidmchi  22733  hmopidmch  22735  hmopidmpj  22736  pjss2coi  22746  pjssmi  22747  pjssge0i  22748  pjidmco  22763  dfpjop  22764  elpjrn  22772  isst  22795  ishst  22796  hstel2  22801  stj  22817  mdbr  22876  mdi  22877  mdbr3  22879  dmdbr  22881  dmdmd  22882  dmdi  22884  dmdbr3  22887  mddmd2  22891  mdsl1i  22903  chjatom  22939  bcm1n  23034  xmulcand  23106  iuninc  23160  fmptcof2  23231  cnre2csqlem  23296  mndpluscn  23301  xrsmulgzz  23309  esumpr2  23441  esumcvg  23456  ofcfeqd2  23464  ismeas  23532  isrnmeas  23533  measvun  23539  probun  23624  subfacp1lem3  23715  subfacp1lem4  23716  subfacp1lem5  23717  subfacp1lem6  23718  subfacval2  23720  erdszelem9  23732  sconpht  23762  ptpcon  23766  cvmliftmolem1  23814  cvmliftmolem2  23815  cvmliftlem10  23827  cvmlift2  23849  cvmliftphtlem  23850  iseupa  23883  eupaseg  23890  eupap1  23902  eupath2  23906  ghomgrpilem1  23994  relexpsucr  24028  relexpsucl  24030  relexpcnv  24031  relexpadd  24037  sqdivzi  24081  mulcan2g  24087  fprb  24131  rdgprc  24153  dfrdg2  24154  preddowncl  24198  poseq  24255  soseq  24256  wfr3g  24257  wfrlem1  24258  wfrlem12  24269  wfrlem14  24271  wfrlem15  24272  wfr2  24275  wfr2c  24276  tfr3ALT  24281  frr3g  24282  frrlem1  24283  frrlem11  24295  sltval2  24312  sltres  24320  nofulllem5  24362  fvsingle  24461  fullfunfv  24487  brcgr  24530  brbtwn2  24535  colinearalglem1  24536  colinearalg  24540  ax5seglem1  24558  ax5seglem2  24559  ax5seglem8  24566  ax5seglem9  24567  axlowdimlem13  24584  axlowdimlem16  24587  axlowdim1  24589  axcontlem1  24594  axcontlem2  24595  axcontlem6  24599  axcontlem7  24600  axcontlem8  24601  lineelsb2  24773  bpolyval  24786  bpolydif  24792  rankung  24798  ranksng  24799  rankpwg  24801  surjsec2  25131  repfuntw  25171  islatalg  25194  labss1  25200  labss2  25202  prodeq3ii  25319  iscom  25344  iscomb  25345  ridlideq  25346  smgrpass2  25352  fprodadd  25363  mndoass2  25371  fprodneg  25389  fprodsub  25390  trooo  25405  rltrooo  25426  com2i  25427  vecval1b  25462  vecval3b  25463  vecax5b  25470  glmrngo  25493  vecax5c  25494  vri  25503  cnegvex2  25671  rnegvex2  25672  cnegvex2b  25673  rnegvex2b  25674  addcanri  25677  addcanrg  25678  isded  25747  dedi  25748  1ded  25749  idosd  25755  domcmpd  25757  codcmpd  25758  iscatOLD  25765  cati  25766  1cat  25770  cmpasso  25784  cmpida  25785  cmpidb  25786  ismona  25820  ismonb  25821  idmon  25828  isepia  25830  isepib  25831  isiso  25836  cinvlem1  25839  cinvlem2  25840  isfuna  25845  isfunb  25846  issrc  25878  propsrc  25879  isntr  25884  cmp2morp  25969  rocatval  25970  cmppar3  25985  selsubf3g  26003  pgapspf2  26064  xsyysx  26156  opnregcld  26259  cldregopn  26260  neibastop3  26322  cocanfo  26385  upixp  26414  sdclem2  26463  caushft  26488  ismtycnv  26537  ismtyima  26538  ismtybndlem  26541  ismtyres  26543  bfplem2  26558  bfp  26559  grpoeqdivid  26582  ghomco  26584  rngohomval  26606  isrngohom  26607  rngohomadd  26611  rngohommul  26612  iscringd  26635  crngocom  26637  crngohomfo  26642  dmncan2  26713  fnelfp  26766  ismrcd2  26785  ismrc  26787  dvdsrabdioph  26902  fphpdo  26911  rmxypairf1o  27007  monotoddzzfi  27038  monotoddzz  27039  oddcomabszz  27040  rmxdioph  27120  expdiophlem2  27126  dnnumch3  27155  aomclem8  27170  islssfg  27179  unxpwdom3  27267  gicabl  27274  pmtrfrn  27411  cntzsdrg  27521  idomodle  27523  fgraphxp  27541  hausgraph  27542  caofcan  27551  expgrowth  27563  fmuldfeq  27724  climmulf  27741  climexp  27742  climsuse  27745  climrecf  27746  stoweidlem30  27790  stoweidlem48  27808  wallispilem4  27828  wallispi2lem1  27831  wallispi2lem2  27832  sbcfun  27996  csbafv12g  28011  csbaovg  28051  bnj1385  28938  bnj66  28965  bnj106  28973  bnj155  28984  bnj222  28988  bnj540  28997  bnj591  29016  bnj594  29017  bnj611  29023  bnj893  29033  bnj1000  29046  bnj966  29049  bnj1112  29086  bnj1234  29116  bnj1253  29120  bnj1280  29123  bnj1326  29129  bnj1450  29153  bnj1463  29158  bnj1529  29173  lshpset  29241  lcvexchlem4  29300  lcvexchlem5  29301  lflset  29322  islfl  29323  lfli  29324  islfld  29325  eqlkr3  29364  isopos  29443  oposlem  29446  opcon3b  29459  cmtvalN  29474  omllaw  29506  cvlexchb2  29594  cvlatexchb2  29598  cvlsupr2  29606  4atlem9  29865  4atlem10a  29866  4atlem11a  29869  4atlem12a  29872  4at2  29876  pmapglb2N  30033  pmapglb2xN  30034  paddasslem17  30098  ispsubclN  30199  ispsubcl2N  30209  lhpmod2i2  30300  lhpmod6i1  30301  4atexlemex2  30333  4atex  30338  4atex2-0aOLDN  30340  4atex2-0cOLDN  30342  ldilval  30375  ltrnfset  30379  ltrnset  30380  isltrn  30381  ltrneq2  30410  trnfsetN  30417  trnsetN  30418  istrnN  30419  cdlemd5  30464  cdleme0moN  30487  cdleme0nex  30552  cdleme18d  30557  cdleme31so  30641  cdleme31fv  30652  cdlemg2jlemOLDN  30855  cdlemg2fvlem  30856  cdlemg2klem  30857  istendo  31022  tendovalco  31027  tendoeq2  31036  dicelvalN  31441  dihval  31495  dihcnv11  31538  dihmeetlem13N  31582  dihlspsnat  31596  dochn0nv  31638  dochkrshp4  31652  lpolsetN  31745  lpolsatN  31751  lpolpolsatN  31752  lcfl1lem  31754  lclkrlem2a  31770  lclkrlem2e  31774  lcfls1lem  31797  lclkrs2  31803  lcdfval  31851  lcdval  31852  mapdffval  31889  mapdfval  31890  mapd0  31928  mapdpglem30  31965  mapdhval  31987  mapdheq2  31992  hdmap1vallem  32061  hdmap1val  32062  hdmap1cbv  32066  hdmapval3N  32104  hdmap10  32106  hdmapeq0  32110  hdmap14lem12  32145  hdmap14lem13  32146  hgmapfval  32152  hgmapvs  32157  hgmapvv  32192  hlhilocv  32223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2278
  Copyright terms: Public domain W3C validator