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

Theorem eqeq12d 2297
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 2295 . 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 1623
This theorem is referenced by:  cdeqeq  2986  sbceqg  3097  csbing  3376  csbifg  3593  uniprg  3842  unisng  3844  intprg  3896  iununi  3986  csbopabg  4094  limeq  4404  ordunisuc  4623  onsucuni2  4625  orduninsuc  4634  csbima12g  5022  dmsnsnsn  5151  cnvsng  5158  csbiotag  5248  csbfv12gALT  5536  fveqres  5560  fvmptf  5616  eqfnfv2f  5626  fvreseq  5628  fmptco  5691  fnressn  5705  fvsng  5714  fnsuppres  5732  cocan1  5801  cocan2  5802  fliftfun  5811  weniso  5852  csbovg  5889  eqfnov  5950  ovmpt2s  5971  ov2gf  5972  ovmpt2dxf  5973  caovcomg  6015  caovassg  6018  caovcang  6021  caovcanrd  6023  caovcan  6024  caovdig  6034  caovdirg  6037  caovmo  6057  grprinvlem  6058  grprinvd  6059  offveqb  6099  caofid0l  6105  caofid0r  6106  caofass  6111  caonncan  6115  op1stg  6132  op2ndg  6133  opabiota  6293  csbriotag  6317  onfununi  6358  tfrlem1  6391  tfrlem2  6392  tfrlem3  6393  tfrlem3a  6394  tfrlem9  6401  tfrlem11  6404  tfrlem12  6405  tfr3  6415  tz7.44-1  6419  tz7.44-2  6420  tz7.44-3  6421  rdglem1  6428  rdg0g  6440  seqomlem1  6462  abianfp  6471  oalim  6531  omlim  6532  oelim  6533  oa0r  6537  om0r  6538  om1r  6541  oaass  6559  oarec  6560  odi  6577  omass  6578  oelim2  6593  oeoalem  6594  oeoa  6595  oeoelem  6596  oeoe  6597  nna0r  6607  nnacom  6615  nnaass  6620  nndi  6621  nnmass  6622  nnmsucr  6623  nnmcom  6624  oaabs  6642  oaabs2  6643  omabs  6645  ecovcom  6769  ecovass  6770  ecovdi  6771  dom2lem  6901  unxpdomlem2  7068  unxpdomlem3  7069  ixpfi2  7154  fipreima  7161  ordiso2  7230  wemaplem1  7261  wemaplem2  7262  wemapso2lem  7265  cantnfval2  7370  cantnfp1lem3  7382  oemapvali  7386  cantnflem1c  7389  cantnflem1  7391  wemapwe  7400  tcvalg  7423  rankvalg  7489  rankonidlem  7500  ranklim  7516  rankuni  7535  cardprclem  7612  cardprc  7613  carduni  7614  fseqenlem1  7651  fodomacn  7683  alephcard  7697  alephfp2  7736  alephval3  7737  dfac12lem1  7769  dfac12lem2  7770  dfac12r  7772  ackbij1lem5  7850  ackbij1lem8  7853  ackbij1lem14  7859  ackbij1lem16  7861  ackbij2lem3  7867  cardcf  7878  sornom  7903  fin23lem28  7966  isf32lem2  7980  itunitc  8047  ituniiun  8048  axdc3lem2  8077  axdc4lem  8081  ttukeylem3  8138  ttukey2g  8143  fpwwe2lem8  8259  fpwwecbv  8266  canth4  8269  pwfseqlem2  8281  addcanpi  8523  mulcanpi  8524  recrecnq  8591  ltexnq  8599  genpv  8623  0idsr  8719  1idsr  8720  ax1rid  8783  mulid1  8835  addcan  8996  addcan2  8997  mulcand  9401  mulcan2d  9402  div11  9450  divmuleq  9465  conjmul  9477  eqneg  9480  ofsubeq0  9743  rpnnen1  10347  cnref1o  10349  xmulasslem  10605  xmulass  10607  xadddi2  10617  prunioo  10764  fzsuc2  10842  fzprval  10844  fztpval  10845  modadd1  11001  modmul1  11002  om2uzsuci  11011  om2uzrdg  11019  uzrdgxfr  11029  seq1  11059  seqp1  11061  seqfveq2  11068  seqfveq  11070  seqshft2  11072  seqsplit  11079  seqcaopr3  11081  seqcaopr2  11082  seqf1olem2a  11084  seqf1olem2  11086  seqf1o  11087  seqid  11091  seqid2  11092  seqhomo  11093  ser1const  11102  mulexp  11141  expadd  11144  expmul  11147  binom2  11218  sq01  11223  modexp  11236  bcpasc  11333  hashgadd  11359  hashdom  11361  hashfzo  11383  hashxplem  11385  hashxp  11386  hashmap  11387  hashpw  11388  hashbclem  11390  hashbc  11391  hashfacen  11392  hashf1lem1  11393  hashf1lem2  11394  hashf1  11395  seqcoll  11401  ccatopth  11462  ccatopth2  11463  cats1un  11476  replim  11601  cjreb  11608  cjexp  11635  absexp  11789  abs1m  11819  recan  11820  isercoll2  12142  iseraltlem2  12155  iseraltlem3  12156  sumeq2w  12165  sumeq2ii  12166  zsum  12191  fsum  12193  fsumf1o  12196  sumss  12197  fsumcvg2  12200  fsumadd  12211  isummulc2  12225  fsum2d  12234  fsummulc2  12246  fsumconst  12252  fsumparts  12264  fsumrelem  12265  fsumiun  12279  binom  12288  bcxmas  12294  incexclem  12295  isumshft  12298  isumnn0nn  12301  climcndslem1  12308  climcndslem2  12309  mertenslem2  12341  efne0  12377  efexp  12381  demoivreALT  12481  moddvds  12538  bitsinv1  12633  sadadd2  12651  smu01lem  12676  smupval  12679  smueqlem  12681  smumullem  12683  gcdaddm  12708  bezoutlem1  12717  bezout  12721  gcddiv  12728  seq1st  12741  alginv  12745  algfx  12750  isprm2lem  12765  nn0gcdsq  12823  crt  12846  eulerthlem2  12850  pythagtriplem1  12869  iserodd  12888  pcqmul  12906  pcexp  12912  pcneg  12926  pcmpt  12940  pcfac  12947  prmreclem2  12964  prmreclem3  12965  1arith  12974  vdwpc  13027  ramcl  13076  imasval  13414  ercpbllem  13450  xpscfv  13464  iscat  13574  iscatd  13575  catideu  13577  iscatd2  13583  catlid  13585  catrid  13586  catass  13588  proplem  13592  homfeq  13597  comfeq  13609  catpropd  13612  moni  13639  epii  13646  sectffval  13653  sectfval  13654  oppcsect  13676  sectmon  13680  isfunc  13738  funcid  13744  funcco  13745  funcpropd  13774  isfull  13784  fthsect  13799  fthmon  13801  natfval  13820  isnat  13821  nati  13829  fucsect  13846  natpropd  13850  setcmon  13919  setcepi  13920  setcsect  13921  evlfcl  13996  uncfcurf  14013  yoniso  14059  isacs5lem  14272  acsdrscl  14273  acsficl  14274  latdisdlem  14292  latdisd  14293  isdlat  14296  dlatmjdi  14297  isps  14311  ismnd  14369  mgmidmo  14370  mndlem1  14371  mgmlrid  14389  ismndd  14396  mndpropd  14398  imasmnd2  14409  ismhm  14417  mhmpropd  14421  mhmlin  14422  mhmeql  14441  gsumvalx  14451  gsumval2  14460  gsumccat  14464  gsumwmhm  14467  frmdgsum  14484  isgrp  14493  grppropd  14500  isgrpd2e  14504  isgrpid2  14518  grpidd2  14519  grpinvfval  14520  grpinvpropd  14543  grpsubrcan  14547  grplactcnv  14564  mulgnn0p1  14578  mulgneg2  14594  mulgnnass  14595  mulgnn0ass  14596  mulgass  14597  mhmmulg  14599  imasgrp2  14610  isghm  14683  ghmlin  14688  ghmeql  14705  isga  14745  gagrpid  14748  gaass  14751  galcan  14758  orbsta  14767  cayleylem2  14788  cntzfval  14796  elcntz  14798  cntzsnval  14800  elcntzsn  14801  cntzi  14805  resscntz  14807  cntzmhm  14814  gsumwrev  14839  odfval  14848  mndodcong  14857  odbezout  14871  odeq1  14873  submod  14880  gexval  14889  gexdvds  14895  ispgp  14903  sylow1lem1  14909  sylow2alem1  14928  sylow2alem2  14929  sylow2blem2  14932  efgmnvl  15023  efgredlemc  15054  efgredeu  15061  frgpuptinv  15080  frgpup1  15084  frgpup3lem  15086  iscmn  15096  cmnpropd  15098  iscmnd  15101  abladdsub4  15115  submcmn2  15135  divsabl  15157  iscyg  15166  cygabl  15177  gsum2d  15223  dmdprd  15236  dprdval  15238  dprdfcntz  15250  subgdmdprd  15269  dprd2da  15277  dpjrid  15297  pgpfac1lem3a  15311  ablfaclem3  15322  ablfac2  15324  isrng  15345  rngpropd  15372  mulgass2  15387  imasrng  15402  dvdsr  15428  dvreq1  15475  isdrng  15516  drngprop  15523  isdrngd  15537  drngpropd  15539  isabv  15584  abvmul  15594  issrng  15615  issrngd  15626  islmod  15631  lmodlema  15632  islmodd  15633  lmodprop2d  15687  islmhm  15784  lmhmlin  15792  islmhm2  15795  lmhmeql  15812  lmhmpropd  15826  islbs  15829  lbspropd  15852  divscrng  15992  islpir  16001  rrgval  16028  unitrrg  16034  isassa  16056  assalem  16057  isassad  16063  assapropd  16067  mvrf1  16170  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  coe1tm  16349  ply1sclf1  16364  cnfldmulg  16406  cnfldexp  16407  prmirredlem  16446  chrcong  16483  zndvds  16503  znf1o  16505  znunit  16517  cygznlem3  16523  frgpcyg  16527  isphl  16532  ipcj  16538  iporthcom  16539  ip2eq  16557  isphld  16558  phlpropd  16559  ocvfval  16566  iscss  16583  ishil  16618  isobs  16620  obsip  16621  obslbs  16630  isperf  16882  restperf  16914  cmpsub  17127  iscon  17139  2ndcsep  17185  elptr2  17269  ptbasin  17272  dfac14  17312  txcnp  17314  ptcnplem  17315  ptcnp  17316  cnmpt11  17357  cnmpt21  17365  cnmptcom  17372  kqfeq  17415  isr0  17428  pt1hmeo  17497  imasdsf1olem  17937  isxms  17993  xmspropd  18019  imasf1oxms  18035  stdbdmopn  18064  isngp3  18120  ngppropd  18153  isnlm  18186  nmvs  18187  xrsxmet  18315  cnheibor  18453  htpyi  18472  htpycc  18478  pi1xfr  18553  pi1coghm  18559  isclm  18562  lmhmclm  18584  clmmulg  18591  iscph  18606  tchcph  18667  cmetcaulem  18714  bcth3  18753  ovolunlem1a  18855  ovolicc2lem1  18876  ovolicc2lem4  18879  ovolicc2  18881  mblsplit  18891  volun  18902  volfiniun  18904  voliunlem1  18907  volsup  18913  ioorinv  18931  uniioombllem2  18938  vitalilem3  18965  mbfeqalem  18997  mbflim  19023  itgeqa  19168  itgconst  19173  itgfsum  19181  itgsplitioo  19192  dvnadd  19278  dvnres  19280  dvexp  19302  dvmptfsum  19322  mvth  19339  dvlip  19340  lhop1lem  19360  dvcvx  19367  evlslem1  19399  mpfrcl  19402  evlsval  19403  mdegle0  19463  ply1nzb  19508  mon1pval  19527  facth1  19550  ig1pval  19558  dgrmulc  19652  dgrcolem1  19654  dgrcolem2  19655  dgrco  19656  coecj  19659  vieta1lem2  19691  vieta1  19692  elqaalem3  19701  dvntaylp  19750  ulmss  19774  mtest  19781  sineq0  19889  efif1olem4  19907  cxpexp  20015  mulcxplem  20031  mulcxp  20032  cxpmul2  20036  cxpeq  20097  affineequiv2  20124  quad2  20135  dcubic  20142  leibpi  20238  o1cxp  20269  scvxcvx  20280  wilthlem1  20306  wilthlem2  20307  perfect  20470  dchrelbas2  20476  dchrinv  20500  dchrptlem2  20504  lgsne0  20572  lgsqrlem2  20581  lgsdchr  20587  lgseisenlem2  20589  lgsquad2lem2  20598  dchrisumlem1  20638  qabvexp  20775  ostthlem1  20776  ostthlem2  20777  ostth3  20787  isgrpo  20863  grpoass  20870  grpoidinvlem3  20873  grpoidinv  20875  grpoideu  20876  grpoidinv2  20885  grpoinvfval  20891  isgrp2d  20902  gxcom  20936  gxinv  20937  gxnn0add  20941  gxnn0mul  20944  isablo  20950  ablocom  20952  gxdi  20963  issubgoilem  20976  isass  20983  opidon  20989  exidu1  20993  cmpidelt  20996  elghomlem2  21029  ghomlin  21031  ghgrplem2  21034  ghgrp  21035  ghablo  21036  isrngo  21045  rngoid  21050  rngoideu  21051  rngodi  21052  rngodir  21053  rngoass  21054  iscom2  21079  vci  21104  vcid  21107  vcdi  21108  vcdir  21109  vcass  21110  isvclem  21133  isnvlem  21166  nvmeq0  21222  nvs  21228  imsmetlem  21259  islno  21331  lnolin  21332  ishmo  21389  isphg  21395  phpar2  21401  phpar  21402  ipdiri  21408  ipasslem1  21409  ipasslem5  21413  ipasslem11  21418  ipassi  21419  dipdir  21420  dipass  21423  ip2eqi  21435  htth  21498  hvsubsub4  21639  hvnegdi  21646  hvaddcan  21649  hvaddcan2  21650  hvsubcan  21653  hvsubcan2  21654  hvaddsub4  21657  hial2eq  21685  normlem9at  21700  normsq  21713  norm-iii  21719  normsub  21722  normpyth  21724  normpar  21734  polid  21738  ococ  21985  chj0  22076  chlejb1  22091  chdmm1  22104  chjass  22112  spanun  22124  spansn  22138  elspansn2  22146  cmbr  22163  cmbr3  22187  pjoml2  22190  pjoml3  22191  osum  22224  spansnj  22226  pjch1  22249  pjadji  22264  pjaddi  22265  pjinormi  22266  pjsubi  22267  pjmuli  22268  pjcjt2  22271  pjch  22273  pjopyth  22299  pjpyth  22304  hoaddcom  22354  hoaddass  22362  hocsubdir  22365  hoaddid1  22371  ho0sub  22377  honegsub  22379  adjsym  22413  eigrei  22414  eigre  22415  eigposi  22416  eigorth  22418  ellnop  22438  elhmop  22453  ellnfn  22463  cnvadj  22472  lnopl  22494  unop  22495  hmop  22502  lnfnl  22511  adj1  22513  eleigvec  22537  hoddi  22570  lnopeq0lem2  22586  lnopunilem1  22590  lnopunilem2  22591  lnopunii  22592  elunop2  22593  lnophmi  22598  lnfnmul  22628  cnlnadjlem5  22651  branmfn  22685  bra11  22688  hmopidmchi  22731  hmopidmch  22733  hmopidmpj  22734  pjss2coi  22744  pjssmi  22745  pjssge0i  22746  pjidmco  22761  dfpjop  22762  elpjrn  22770  isst  22793  ishst  22794  hstel2  22799  stj  22815  mdbr  22874  mdi  22875  mdbr3  22877  dmdbr  22879  dmdmd  22880  dmdi  22882  dmdbr3  22885  mddmd2  22889  mdsl1i  22901  chjatom  22937  bcm1n  23032  xmulcand  23104  iuninc  23158  fmptcof2  23229  cnre2csqlem  23294  mndpluscn  23299  xrsmulgzz  23307  esumpr2  23439  esumcvg  23454  ofcfeqd2  23462  ismeas  23530  isrnmeas  23531  measvun  23537  probun  23622  subfacp1lem3  23713  subfacp1lem4  23714  subfacp1lem5  23715  subfacp1lem6  23716  subfacval2  23718  erdszelem9  23730  sconpht  23760  ptpcon  23764  cvmliftmolem1  23812  cvmliftmolem2  23813  cvmliftlem10  23825  cvmlift2  23847  cvmliftphtlem  23848  iseupa  23881  eupaseg  23888  eupap1  23900  eupath2  23904  ghomgrpilem1  23992  relexpsucr  24026  relexpsucl  24028  relexpcnv  24029  relexpadd  24035  sqdivzi  24079  mulcan2g  24085  fprb  24129  rdgprc  24151  dfrdg2  24152  preddowncl  24196  poseq  24253  soseq  24254  wfr3g  24255  wfrlem1  24256  wfrlem12  24267  wfrlem14  24269  wfrlem15  24270  wfr2  24273  wfr2c  24274  tfr3ALT  24279  frr3g  24280  frrlem1  24281  frrlem11  24293  sltval2  24310  sltres  24318  nofulllem5  24360  fvsingle  24459  fullfunfv  24485  brcgr  24528  brbtwn2  24533  colinearalglem1  24534  colinearalg  24538  ax5seglem1  24556  ax5seglem2  24557  ax5seglem8  24564  ax5seglem9  24565  axlowdimlem13  24582  axlowdimlem16  24585  axlowdim1  24587  axcontlem1  24592  axcontlem2  24593  axcontlem6  24597  axcontlem7  24598  axcontlem8  24599  lineelsb2  24771  bpolyval  24784  bpolydif  24790  rankung  24796  ranksng  24797  rankpwg  24799  surjsec2  25120  repfuntw  25160  islatalg  25183  labss1  25189  labss2  25191  prodeq3ii  25308  iscom  25333  iscomb  25334  ridlideq  25335  smgrpass2  25341  fprodadd  25352  mndoass2  25360  fprodneg  25378  fprodsub  25379  trooo  25394  rltrooo  25415  com2i  25416  vecval1b  25451  vecval3b  25452  vecax5b  25459  glmrngo  25482  vecax5c  25483  vri  25492  cnegvex2  25660  rnegvex2  25661  cnegvex2b  25662  rnegvex2b  25663  addcanri  25666  addcanrg  25667  isded  25736  dedi  25737  1ded  25738  idosd  25744  domcmpd  25746  codcmpd  25747  iscatOLD  25754  cati  25755  1cat  25759  cmpasso  25773  cmpida  25774  cmpidb  25775  ismona  25809  ismonb  25810  idmon  25817  isepia  25819  isepib  25820  isiso  25825  cinvlem1  25828  cinvlem2  25829  isfuna  25834  isfunb  25835  issrc  25867  propsrc  25868  isntr  25873  cmp2morp  25958  rocatval  25959  cmppar3  25974  selsubf3g  25992  pgapspf2  26053  xsyysx  26145  opnregcld  26248  cldregopn  26249  neibastop3  26311  cocanfo  26374  upixp  26403  sdclem2  26452  caushft  26477  ismtycnv  26526  ismtyima  26527  ismtybndlem  26530  ismtyres  26532  bfplem2  26547  bfp  26548  grpoeqdivid  26571  ghomco  26573  rngohomval  26595  isrngohom  26596  rngohomadd  26600  rngohommul  26601  iscringd  26624  crngocom  26626  crngohomfo  26631  dmncan2  26702  fnelfp  26755  ismrcd2  26774  ismrc  26776  dvdsrabdioph  26891  fphpdo  26900  rmxypairf1o  26996  monotoddzzfi  27027  monotoddzz  27028  oddcomabszz  27029  rmxdioph  27109  expdiophlem2  27115  dnnumch3  27144  aomclem8  27159  islssfg  27168  unxpwdom3  27256  gicabl  27263  pmtrfrn  27400  cntzsdrg  27510  idomodle  27512  fgraphxp  27530  hausgraph  27531  caofcan  27540  expgrowth  27552  fmuldfeq  27713  climmulf  27730  climexp  27731  climsuse  27734  climrecf  27735  stoweidlem30  27779  stoweidlem48  27797  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  sbcfun  27985  csbafv12g  28000  csbaovg  28040  bnj1385  28865  bnj66  28892  bnj106  28900  bnj155  28911  bnj222  28915  bnj540  28924  bnj591  28943  bnj594  28944  bnj611  28950  bnj893  28960  bnj1000  28973  bnj966  28976  bnj1112  29013  bnj1234  29043  bnj1253  29047  bnj1280  29050  bnj1326  29056  bnj1450  29080  bnj1463  29085  bnj1529  29100  lshpset  29168  lcvexchlem4  29227  lcvexchlem5  29228  lflset  29249  islfl  29250  lfli  29251  islfld  29252  eqlkr3  29291  isopos  29370  oposlem  29373  opcon3b  29386  cmtvalN  29401  omllaw  29433  cvlexchb2  29521  cvlatexchb2  29525  cvlsupr2  29533  4atlem9  29792  4atlem10a  29793  4atlem11a  29796  4atlem12a  29799  4at2  29803  pmapglb2N  29960  pmapglb2xN  29961  paddasslem17  30025  ispsubclN  30126  ispsubcl2N  30136  lhpmod2i2  30227  lhpmod6i1  30228  4atexlemex2  30260  4atex  30265  4atex2-0aOLDN  30267  4atex2-0cOLDN  30269  ldilval  30302  ltrnfset  30306  ltrnset  30307  isltrn  30308  ltrneq2  30337  trnfsetN  30344  trnsetN  30345  istrnN  30346  cdlemd5  30391  cdleme0moN  30414  cdleme0nex  30479  cdleme18d  30484  cdleme31so  30568  cdleme31fv  30579  cdlemg2jlemOLDN  30782  cdlemg2fvlem  30783  cdlemg2klem  30784  istendo  30949  tendovalco  30954  tendoeq2  30963  dicelvalN  31368  dihval  31422  dihcnv11  31465  dihmeetlem13N  31509  dihlspsnat  31523  dochn0nv  31565  dochkrshp4  31579  lpolsetN  31672  lpolsatN  31678  lpolpolsatN  31679  lcfl1lem  31681  lclkrlem2a  31697  lclkrlem2e  31701  lcfls1lem  31724  lclkrs2  31730  lcdfval  31778  lcdval  31779  mapdffval  31816  mapdfval  31817  mapd0  31855  mapdpglem30  31892  mapdhval  31914  mapdheq2  31919  hdmap1vallem  31988  hdmap1val  31989  hdmap1cbv  31993  hdmapval3N  32031  hdmap10  32033  hdmapeq0  32037  hdmap14lem12  32072  hdmap14lem13  32073  hgmapfval  32079  hgmapvs  32084  hgmapvv  32119  hlhilocv  32150
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-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator