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

Theorem eqeq12d 2401
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 2399 . 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 1649
This theorem is referenced by:  cdeqeq  3099  sbceqg  3210  csbing  3491  csbifg  3710  uniprg  3972  unisng  3974  intprg  4026  iununi  4116  csbopabg  4224  limeq  4534  ordunisuc  4752  onsucuni2  4754  orduninsuc  4763  csbima12g  5153  dmsnsnsn  5288  cnvsng  5295  csbiotag  5387  csbfv12gALT  5679  fveqres  5703  fvmptf  5760  eqfnfv2f  5770  fvreseq  5772  fmptco  5840  fnressn  5857  fvsng  5866  fnpr  5889  fnprOLD  5890  fnsuppres  5891  cocan1  5963  cocan2  5964  fliftfun  5973  weniso  6014  csbovg  6051  eqfnov  6115  ovmpt2s  6136  ov2gf  6137  ovmpt2dxf  6138  caovcomg  6181  caovassg  6184  caovcang  6187  caovcanrd  6189  caovcan  6190  caovdig  6200  caovdirg  6203  caovmo  6223  grprinvlem  6224  grprinvd  6225  offveqb  6265  caofid0l  6271  caofid0r  6272  caofass  6277  caonncan  6281  op1stg  6298  op2ndg  6299  opabiota  6474  csbriotag  6498  onfununi  6539  tfrlem1  6572  tfrlem2  6573  tfrlem3  6574  tfrlem3a  6575  tfrlem9  6582  tfrlem11  6585  tfrlem12  6586  tfr3  6596  tz7.44-1  6600  tz7.44-2  6601  tz7.44-3  6602  rdglem1  6609  rdg0g  6621  seqomlem1  6643  abianfp  6652  oalim  6712  omlim  6713  oelim  6714  oa0r  6718  om0r  6719  om1r  6722  oaass  6740  oarec  6741  odi  6758  omass  6759  oelim2  6774  oeoalem  6775  oeoa  6776  oeoelem  6777  oeoe  6778  nna0r  6788  nnacom  6796  nnaass  6801  nndi  6802  nnmass  6803  nnmsucr  6804  nnmcom  6805  oaabs  6823  oaabs2  6824  omabs  6826  ecovcom  6951  ecovass  6952  ecovdi  6953  dom2lem  7083  unxpdomlem2  7250  unxpdomlem3  7251  ixpfi2  7340  fipreima  7347  ordiso2  7417  wemaplem1  7448  wemaplem2  7449  wemapso2lem  7452  cantnfval2  7557  cantnfp1lem3  7569  oemapvali  7573  cantnflem1c  7576  cantnflem1  7578  wemapwe  7587  tcvalg  7610  rankvalg  7676  rankonidlem  7687  ranklim  7703  rankuni  7722  cardprclem  7799  cardprc  7800  carduni  7801  fseqenlem1  7838  fodomacn  7870  alephcard  7884  alephfp2  7923  alephval3  7924  dfac12lem1  7956  dfac12lem2  7957  dfac12r  7959  ackbij1lem5  8037  ackbij1lem8  8040  ackbij1lem14  8046  ackbij1lem16  8048  ackbij2lem3  8054  cardcf  8065  sornom  8090  fin23lem28  8153  isf32lem2  8167  itunitc  8234  ituniiun  8235  axdc3lem2  8264  axdc4lem  8268  ttukeylem3  8324  ttukey2g  8329  fpwwe2lem8  8445  fpwwecbv  8452  canth4  8455  pwfseqlem2  8467  addcanpi  8709  mulcanpi  8710  recrecnq  8777  ltexnq  8785  genpv  8809  0idsr  8905  1idsr  8906  ax1rid  8969  mulid1  9021  addcan  9182  addcan2  9183  mulcand  9587  mulcan2d  9588  div11  9636  divmuleq  9651  conjmul  9663  eqneg  9666  ofsubeq0  9929  rpnnen1  10537  cnref1o  10539  xmulasslem  10796  xmulass  10798  xadddi2  10808  prunioo  10957  fzsuc2  11035  fzprval  11037  fztpval  11038  modadd1  11205  modmul1  11206  om2uzsuci  11215  om2uzrdg  11223  uzrdgxfr  11233  seq1  11263  seqp1  11265  seqfveq2  11272  seqfveq  11274  seqshft2  11276  seqsplit  11283  seqcaopr3  11285  seqcaopr2  11286  seqf1olem2a  11288  seqf1olem2  11290  seqf1o  11291  seqid  11295  seqid2  11296  seqhomo  11297  ser1const  11306  seqof2  11308  mulexp  11346  expadd  11349  expmul  11352  binom2  11423  sq01  11428  modexp  11441  bcpasc  11539  hashgadd  11578  hashdom  11580  hashfzo  11621  hashxplem  11623  hashxp  11624  hashmap  11625  hashpw  11626  hashbclem  11628  hashbc  11629  hashfacen  11630  hashf1lem1  11631  hashf1lem2  11632  hashf1  11633  seqcoll  11639  ccatopth  11703  ccatopth2  11704  cats1un  11717  replim  11848  cjreb  11855  cjexp  11882  absexp  12036  abs1m  12066  recan  12067  isercoll2  12389  iseraltlem2  12403  iseraltlem3  12404  sumeq2w  12413  sumeq2ii  12414  zsum  12439  fsum  12441  fsumf1o  12444  sumss  12445  fsumcvg2  12448  fsumadd  12459  isummulc2  12473  fsum2d  12482  fsummulc2  12494  fsumconst  12500  fsumparts  12512  fsumrelem  12513  fsumiun  12527  binom  12536  bcxmas  12542  incexclem  12543  isumshft  12546  isumnn0nn  12549  climcndslem1  12556  climcndslem2  12557  mertenslem2  12589  efne0  12625  efexp  12629  demoivreALT  12729  moddvds  12786  bitsinv1  12881  sadadd2  12899  smu01lem  12924  smupval  12927  smueqlem  12929  smumullem  12931  gcdaddm  12956  bezoutlem1  12965  bezout  12969  gcddiv  12976  seq1st  12989  alginv  12993  algfx  12998  isprm2lem  13013  nn0gcdsq  13071  crt  13094  eulerthlem2  13098  pythagtriplem1  13117  iserodd  13136  pcqmul  13154  pcexp  13160  pcneg  13174  pcmpt  13188  pcfac  13195  prmreclem2  13212  prmreclem3  13213  1arith  13222  vdwpc  13275  ramcl  13324  imasval  13664  ercpbllem  13700  xpscfv  13714  iscat  13824  iscatd  13825  catideu  13827  iscatd2  13833  catlid  13835  catrid  13836  catass  13838  proplem  13842  homfeq  13847  comfeq  13859  catpropd  13862  moni  13889  epii  13896  sectffval  13903  sectfval  13904  oppcsect  13926  sectmon  13930  isfunc  13988  funcid  13994  funcco  13995  funcpropd  14024  isfull  14034  fthsect  14049  fthmon  14051  natfval  14070  isnat  14071  nati  14079  fucsect  14096  natpropd  14100  setcmon  14169  setcepi  14170  setcsect  14171  evlfcl  14246  uncfcurf  14263  yoniso  14309  isacs5lem  14522  acsdrscl  14523  acsficl  14524  latdisdlem  14542  latdisd  14543  isdlat  14546  dlatmjdi  14547  isps  14561  ismnd  14619  mgmidmo  14620  mndlem1  14621  mgmlrid  14639  ismndd  14646  mndpropd  14648  imasmnd2  14659  ismhm  14667  mhmpropd  14671  mhmlin  14672  mhmeql  14691  gsumvalx  14701  gsumval2  14710  gsumccat  14714  gsumwmhm  14717  frmdgsum  14734  isgrp  14743  grppropd  14750  isgrpd2e  14754  isgrpid2  14768  grpidd2  14769  grpinvfval  14770  grpinvpropd  14793  grpsubrcan  14797  grplactcnv  14814  mulgnn0p1  14828  mulgneg2  14844  mulgnnass  14845  mulgnn0ass  14846  mulgass  14847  mhmmulg  14849  imasgrp2  14860  isghm  14933  ghmlin  14938  ghmeql  14955  isga  14995  gagrpid  14998  gaass  15001  galcan  15008  orbsta  15017  cayleylem2  15038  cntzfval  15046  elcntz  15048  cntzsnval  15050  elcntzsn  15051  cntzi  15055  resscntz  15057  cntzmhm  15064  gsumwrev  15089  odfval  15098  mndodcong  15107  odbezout  15121  odeq1  15123  submod  15130  gexval  15139  gexdvds  15145  ispgp  15153  sylow1lem1  15159  sylow2alem1  15178  sylow2alem2  15179  sylow2blem2  15182  efgmnvl  15273  efgredlemc  15304  efgredeu  15311  frgpuptinv  15330  frgpup1  15334  frgpup3lem  15336  iscmn  15346  cmnpropd  15348  iscmnd  15351  abladdsub4  15365  submcmn2  15385  divsabl  15407  iscyg  15416  cygabl  15427  gsum2d  15473  dmdprd  15486  dprdval  15488  dprdfcntz  15500  subgdmdprd  15519  dprd2da  15527  dpjrid  15547  pgpfac1lem3a  15561  ablfaclem3  15572  ablfac2  15574  isrng  15595  rngpropd  15622  mulgass2  15637  imasrng  15652  dvdsr  15678  dvreq1  15725  isdrng  15766  drngprop  15773  isdrngd  15787  drngpropd  15789  isabv  15834  abvmul  15844  issrng  15865  issrngd  15876  islmod  15881  lmodlema  15882  islmodd  15883  lmodprop2d  15933  islmhm  16030  lmhmlin  16038  islmhm2  16041  lmhmeql  16058  lmhmpropd  16072  islbs  16075  lbspropd  16098  divscrng  16238  islpir  16247  rrgval  16274  unitrrg  16280  isassa  16302  assalem  16303  isassad  16309  assapropd  16313  mvrf1  16416  mplmonmul  16454  mplcoe1  16455  mplcoe3  16456  mplcoe2  16457  coe1tm  16592  ply1sclf1  16607  cnfldmulg  16656  cnfldexp  16657  prmirredlem  16696  chrcong  16733  zndvds  16753  znf1o  16755  znunit  16767  cygznlem3  16773  frgpcyg  16777  isphl  16782  ipcj  16788  iporthcom  16789  ip2eq  16807  isphld  16808  phlpropd  16809  ocvfval  16816  iscss  16833  ishil  16868  isobs  16870  obsip  16871  obslbs  16880  isperf  17137  restperf  17170  cmpsub  17385  iscon  17397  2ndcsep  17443  elptr2  17527  ptbasin  17530  dfac14  17571  txcnp  17573  ptcnplem  17574  ptcnp  17575  cnmpt11  17616  cnmpt21  17624  cnmptcom  17631  kqfeq  17677  isr0  17690  pt1hmeo  17759  ustexsym  18166  isusp  18212  imasdsf1olem  18311  isxms  18367  xmspropd  18393  imasf1oxms  18409  stdbdmopn  18438  isngp3  18516  ngppropd  18549  isnlm  18582  nmvs  18583  xrsxmet  18711  cnheibor  18851  htpyi  18870  htpycc  18876  pi1xfr  18951  pi1coghm  18957  isclm  18960  lmhmclm  18982  clmmulg  18989  iscph  19004  tchcph  19065  cmetcaulem  19112  bcth3  19153  ovolunlem1a  19259  ovolicc2lem1  19280  ovolicc2lem4  19283  ovolicc2  19285  mblsplit  19295  volun  19306  volfiniun  19308  voliunlem1  19311  volsup  19317  ioorinv  19335  uniioombllem2  19342  vitalilem3  19369  mbfeqalem  19401  mbflim  19427  itgeqa  19572  itgconst  19577  itgfsum  19585  itgsplitioo  19596  dvnadd  19682  dvnres  19684  dvexp  19706  dvmptfsum  19726  mvth  19743  dvlip  19744  lhop1lem  19764  dvcvx  19771  evlslem1  19803  mpfrcl  19806  evlsval  19807  mdegle0  19867  ply1nzb  19912  mon1pval  19931  facth1  19954  ig1pval  19962  dgrmulc  20056  dgrcolem1  20058  dgrcolem2  20059  dgrco  20060  coecj  20063  vieta1lem2  20095  vieta1  20096  elqaalem3  20105  dvntaylp  20154  ulmss  20180  mtest  20187  sineq0  20296  efif1olem4  20314  cxpexp  20426  mulcxplem  20442  mulcxp  20443  cxpmul2  20447  cxpeq  20508  affineequiv2  20535  quad2  20546  dcubic  20553  leibpi  20649  o1cxp  20680  scvxcvx  20691  wilthlem1  20718  wilthlem2  20719  perfect  20882  dchrelbas2  20888  dchrinv  20912  dchrptlem2  20916  lgsne0  20984  lgsqrlem2  20993  lgsdchr  20999  lgseisenlem2  21001  lgsquad2lem2  21010  dchrisumlem1  21050  qabvexp  21187  ostthlem1  21188  ostthlem2  21189  ostth3  21199  usgraidx2v  21278  nbgraf1olem5  21321  cusgrasize  21353  wlkntrllem4  21416  constr1trl  21436  constr2trl  21446  redwlk  21454  wlkdvspthlem  21455  iscrct  21459  iscycl  21460  fargshiftf1  21472  fargshiftfva  21474  usgrcyclnl2  21476  3v3e3cycl1  21479  constr3trllem5  21489  4cycl4v4e  21501  4cycl4dv4e  21503  iseupa  21535  eupatrl  21538  eupaseg  21543  eupap1  21546  eupath2  21550  isgrpo  21632  grpoass  21639  grpoidinvlem3  21642  grpoidinv  21644  grpoideu  21645  grpoidinv2  21654  grpoinvfval  21660  isgrp2d  21671  gxcom  21705  gxinv  21706  gxnn0add  21710  gxnn0mul  21713  isablo  21719  ablocom  21721  gxdi  21732  issubgoilem  21745  isass  21752  opidon  21758  exidu1  21762  cmpidelt  21765  elghomlem2  21798  ghomlin  21800  ghgrplem2  21803  ghgrp  21804  ghablo  21805  isrngo  21814  rngoid  21819  rngoideu  21820  rngodi  21821  rngodir  21822  rngoass  21823  iscom2  21848  vci  21875  vcid  21878  vcdi  21879  vcdir  21880  vcass  21881  isvclem  21904  isnvlem  21937  nvmeq0  21993  nvs  21999  imsmetlem  22030  islno  22102  lnolin  22103  ishmo  22160  isphg  22166  phpar2  22172  phpar  22173  ipdiri  22179  ipasslem1  22180  ipasslem5  22184  ipasslem11  22189  ipassi  22190  dipdir  22191  dipass  22194  ip2eqi  22206  htth  22269  hvsubsub4  22410  hvnegdi  22417  hvaddcan  22420  hvaddcan2  22421  hvsubcan  22424  hvsubcan2  22425  hvaddsub4  22428  hial2eq  22456  normlem9at  22471  normsq  22484  norm-iii  22490  normsub  22493  normpyth  22495  normpar  22505  polid  22509  ococ  22756  chj0  22847  chlejb1  22862  chdmm1  22875  chjass  22883  spanun  22895  spansn  22909  elspansn2  22917  cmbr  22934  cmbr3  22958  pjoml2  22961  pjoml3  22962  osum  22995  spansnj  22997  pjch1  23020  pjadji  23035  pjaddi  23036  pjinormi  23037  pjsubi  23038  pjmuli  23039  pjcjt2  23042  pjch  23044  pjopyth  23070  pjpyth  23075  hoaddcom  23125  hoaddass  23133  hocsubdir  23136  hoaddid1  23142  ho0sub  23148  honegsub  23150  adjsym  23184  eigrei  23185  eigre  23186  eigposi  23187  eigorth  23189  ellnop  23209  elhmop  23224  ellnfn  23234  cnvadj  23243  lnopl  23265  unop  23266  hmop  23273  lnfnl  23282  adj1  23284  eleigvec  23308  hoddi  23341  lnopeq0lem2  23357  lnopunilem1  23361  lnopunilem2  23362  lnopunii  23363  elunop2  23364  lnophmi  23369  lnfnmul  23399  cnlnadjlem5  23422  branmfn  23456  bra11  23459  hmopidmchi  23502  hmopidmch  23504  hmopidmpj  23505  pjss2coi  23515  pjssmi  23516  pjssge0i  23517  pjidmco  23532  dfpjop  23533  elpjrn  23541  isst  23564  ishst  23565  hstel2  23570  stj  23586  mdbr  23645  mdi  23646  mdbr3  23648  dmdbr  23650  dmdmd  23651  dmdi  23653  dmdbr3  23656  mddmd2  23660  mdsl1i  23672  chjatom  23708  iuninc  23855  fmptcof2  23918  bcm1n  23987  xmulcand  24005  xrsmulgzz  24033  cnre2csqlem  24112  mndpluscn  24116  qqhval2  24165  esumfzf  24255  esumcvg  24272  ofcfeqd2  24280  ismeas  24349  isrnmeas  24350  measvun  24357  probun  24456  facgam  24629  subfacp1lem3  24647  subfacp1lem4  24648  subfacp1lem5  24649  subfacp1lem6  24650  subfacval2  24652  erdszelem9  24664  sconpht  24695  ptpcon  24699  cvmliftmolem1  24747  cvmliftmolem2  24748  cvmliftlem10  24760  cvmlift2  24782  cvmliftphtlem  24783  ghomgrpilem1  24875  relexpsucr  24909  relexpsucl  24911  relexpcnv  24912  relexpadd  24917  sqdivzi  24963  mulcan2g  24969  shftvalg  24987  clim2prod  24995  prodfrec  25002  prodeq2w  25017  prodeq2ii  25018  zprod  25042  fprod  25046  fprodf1o  25051  fprodser  25054  fprodmul  25063  fproddiv  25064  prodsn  25065  fprodabs  25076  fprodefsum  25077  fprodconst  25081  faclimlem1  25120  fprb  25153  rdgprc  25175  dfrdg2  25176  preddowncl  25220  poseq  25277  soseq  25278  wfr3g  25279  wfrlem1  25280  wfrlem12  25291  wfrlem14  25293  wfrlem15  25294  wfr2  25297  wfr2c  25298  tfr3ALT  25303  frr3g  25304  frrlem1  25305  frrlem11  25317  sltval2  25334  sltres  25342  nofulllem5  25384  fvsingle  25483  fullfunfv  25510  brcgr  25553  brbtwn2  25558  colinearalglem1  25559  colinearalg  25563  ax5seglem1  25581  ax5seglem2  25582  ax5seglem8  25589  ax5seglem9  25590  axlowdimlem13  25607  axlowdimlem16  25610  axlowdim1  25612  axcontlem1  25617  axcontlem2  25618  axcontlem6  25622  axcontlem7  25623  axcontlem8  25624  lineelsb2  25796  bpolyval  25809  bpolydif  25815  rankung  25821  ranksng  25822  rankpwg  25824  voliunnfl  25955  volsupnfl  25956  opnregcld  26024  cldregopn  26025  neibastop3  26082  cocanfo  26110  upixp  26122  sdclem2  26137  caushft  26158  ismtycnv  26202  ismtyima  26203  ismtybndlem  26206  ismtyres  26208  bfplem2  26223  bfp  26224  grpoeqdivid  26247  ghomco  26249  rngohomval  26271  isrngohom  26272  rngohomadd  26276  rngohommul  26277  iscringd  26300  crngocom  26302  crngohomfo  26307  dmncan2  26378  fnelfp  26427  ismrcd2  26444  ismrc  26446  dvdsrabdioph  26561  fphpdo  26569  rmxypairf1o  26665  monotoddzzfi  26696  monotoddzz  26697  oddcomabszz  26698  rmxdioph  26778  expdiophlem2  26784  dnnumch3  26813  aomclem8  26828  islssfg  26837  unxpwdom3  26925  gicabl  26932  pmtrfrn  27069  cntzsdrg  27179  idomodle  27181  fgraphxp  27199  hausgraph  27200  caofcan  27209  expgrowth  27221  fmuldfeq  27381  climmulf  27398  climexp  27399  climsuse  27402  climrecf  27403  stoweidlem30  27447  stoweidlem48  27465  wallispilem4  27485  wallispi2lem1  27488  wallispi2lem2  27489  csbafv12g  27670  csbaovg  27713  2pthfrgra  27764  bnj1385  28542  bnj66  28569  bnj106  28577  bnj155  28588  bnj222  28592  bnj540  28601  bnj591  28620  bnj594  28621  bnj611  28627  bnj893  28637  bnj1000  28650  bnj966  28653  bnj1112  28690  bnj1234  28720  bnj1253  28724  bnj1280  28727  bnj1326  28733  bnj1450  28757  bnj1463  28762  bnj1529  28777  lshpset  29093  lcvexchlem4  29152  lcvexchlem5  29153  lflset  29174  islfl  29175  lfli  29176  islfld  29177  eqlkr3  29216  isopos  29295  oposlem  29298  opcon3b  29311  cmtvalN  29326  omllaw  29358  cvlexchb2  29446  cvlatexchb2  29450  cvlsupr2  29458  4atlem9  29717  4atlem10a  29718  4atlem11a  29721  4atlem12a  29724  4at2  29728  pmapglb2N  29885  pmapglb2xN  29886  paddasslem17  29950  ispsubclN  30051  ispsubcl2N  30061  lhpmod2i2  30152  lhpmod6i1  30153  4atexlemex2  30185  4atex  30190  4atex2-0aOLDN  30192  4atex2-0cOLDN  30194  ldilval  30227  ltrnfset  30231  ltrnset  30232  isltrn  30233  ltrneq2  30262  trnfsetN  30269  trnsetN  30270  istrnN  30271  cdlemd5  30316  cdleme0moN  30339  cdleme0nex  30404  cdleme18d  30409  cdleme31so  30493  cdleme31fv  30504  cdlemg2jlemOLDN  30707  cdlemg2fvlem  30708  cdlemg2klem  30709  istendo  30874  tendovalco  30879  tendoeq2  30888  dicelvalN  31293  dihval  31347  dihcnv11  31390  dihmeetlem13N  31434  dihlspsnat  31448  dochn0nv  31490  dochkrshp4  31504  lpolsetN  31597  lpolsatN  31603  lpolpolsatN  31604  lcfl1lem  31606  lclkrlem2a  31622  lclkrlem2e  31626  lcfls1lem  31649  lclkrs2  31655  lcdfval  31703  lcdval  31704  mapdffval  31741  mapdfval  31742  mapd0  31780  mapdpglem30  31817  mapdhval  31839  mapdheq2  31844  hdmap1vallem  31913  hdmap1val  31914  hdmap1cbv  31918  hdmapval3N  31956  hdmap10  31958  hdmapeq0  31962  hdmap14lem12  31997  hdmap14lem13  31998  hgmapfval  32004  hgmapvs  32009  hgmapvv  32044  hlhilocv  32075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2380
  Copyright terms: Public domain W3C validator