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

Theorem eqeq12d 2298
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 2296 . 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  2987  sbceqg  3098  csbing  3377  csbifg  3594  uniprg  3843  unisng  3845  intprg  3897  iununi  3987  csbopabg  4095  limeq  4403  ordunisuc  4622  onsucuni2  4624  orduninsuc  4633  csbima12g  5021  dmsnsnsn  5149  cnvsng  5156  fv2  5482  csbfv12g  5496  csbfv12gALT  5497  fveqres  5522  fvmptf  5578  eqfnfv2f  5588  fvreseq  5590  fmptco  5653  fnressn  5667  fvsng  5676  fnsuppres  5694  cocan1  5763  cocan2  5764  fliftfun  5773  weniso  5814  csbovg  5851  eqfnov  5912  ovmpt2s  5933  ov2gf  5934  ovmpt2dxf  5935  caovcomg  5977  caovassg  5980  caovcang  5983  caovcanrd  5985  caovcan  5986  caovdig  5996  caovdirg  5999  caovmo  6019  grprinvlem  6020  grprinvd  6021  offveqb  6061  caofid0l  6067  caofid0r  6068  caofass  6073  caonncan  6077  op1stg  6094  op2ndg  6095  opabiota  6287  csbriotag  6313  onfununi  6354  tfrlem1  6387  tfrlem2  6388  tfrlem3  6389  tfrlem3a  6390  tfrlem9  6397  tfrlem11  6400  tfrlem12  6401  tfr3  6411  tz7.44-1  6415  tz7.44-2  6416  tz7.44-3  6417  rdglem1  6424  rdg0g  6436  seqomlem1  6458  abianfp  6467  oalim  6527  omlim  6528  oelim  6529  oa0r  6533  om0r  6534  om1r  6537  oaass  6555  oarec  6556  odi  6573  omass  6574  oelim2  6589  oeoalem  6590  oeoa  6591  oeoelem  6592  oeoe  6593  nna0r  6603  nnacom  6611  nnaass  6616  nndi  6617  nnmass  6618  nnmsucr  6619  nnmcom  6620  oaabs  6638  oaabs2  6639  omabs  6641  ecovcom  6765  ecovass  6766  ecovdi  6767  dom2lem  6897  unxpdomlem2  7064  unxpdomlem3  7065  ixpfi2  7150  fipreima  7157  ordiso2  7226  wemaplem1  7257  wemaplem2  7258  wemapso2lem  7261  cantnfval2  7366  cantnfp1lem3  7378  oemapvali  7382  cantnflem1c  7385  cantnflem1  7387  wemapwe  7396  tcvalg  7419  rankvalg  7485  rankonidlem  7496  ranklim  7512  rankuni  7531  cardprclem  7608  cardprc  7609  carduni  7610  fseqenlem1  7647  fodomacn  7679  alephcard  7693  alephfp2  7732  alephval3  7733  dfac12lem1  7765  dfac12lem2  7766  dfac12r  7768  ackbij1lem5  7846  ackbij1lem8  7849  ackbij1lem14  7855  ackbij1lem16  7857  ackbij2lem3  7863  cardcf  7874  sornom  7899  fin23lem28  7962  isf32lem2  7976  itunitc  8043  ituniiun  8044  axdc3lem2  8073  axdc4lem  8077  ttukeylem3  8134  ttukey2g  8139  fpwwe2lem8  8255  fpwwecbv  8262  canth4  8265  pwfseqlem2  8277  addcanpi  8519  mulcanpi  8520  recrecnq  8587  ltexnq  8595  genpv  8619  0idsr  8715  1idsr  8716  ax1rid  8779  mulid1  8831  addcan  8992  addcan2  8993  mulcand  9397  mulcan2d  9398  div11  9446  divmuleq  9461  conjmul  9473  eqneg  9476  ofsubeq0  9739  rpnnen1  10343  cnref1o  10345  xmulasslem  10601  xmulass  10603  xadddi2  10613  prunioo  10760  fzsuc2  10838  fzprval  10840  fztpval  10841  modadd1  10997  modmul1  10998  om2uzsuci  11007  om2uzrdg  11015  uzrdgxfr  11025  seq1  11055  seqp1  11057  seqfveq2  11064  seqfveq  11066  seqshft2  11068  seqsplit  11075  seqcaopr3  11077  seqcaopr2  11078  seqf1olem2a  11080  seqf1olem2  11082  seqf1o  11083  seqid  11087  seqid2  11088  seqhomo  11089  ser1const  11098  mulexp  11137  expadd  11140  expmul  11143  binom2  11214  sq01  11219  modexp  11232  bcpasc  11329  hashgadd  11355  hashdom  11357  hashfzo  11379  hashxplem  11381  hashxp  11382  hashmap  11383  hashpw  11384  hashbclem  11386  hashbc  11387  hashfacen  11388  hashf1lem1  11389  hashf1lem2  11390  hashf1  11391  seqcoll  11397  ccatopth  11458  ccatopth2  11459  cats1un  11472  replim  11597  cjreb  11604  cjexp  11631  absexp  11785  abs1m  11815  recan  11816  isercoll2  12138  iseraltlem2  12151  iseraltlem3  12152  sumeq2w  12161  sumeq2ii  12162  zsum  12187  fsum  12189  fsumf1o  12192  sumss  12193  fsumcvg2  12196  fsumadd  12207  isummulc2  12221  fsum2d  12230  fsummulc2  12242  fsumconst  12248  fsumparts  12260  fsumrelem  12261  fsumiun  12275  binom  12284  bcxmas  12290  incexclem  12291  isumshft  12294  isumnn0nn  12297  climcndslem1  12304  climcndslem2  12305  mertenslem2  12337  efne0  12373  efexp  12377  demoivreALT  12477  moddvds  12534  bitsinv1  12629  sadadd2  12647  smu01lem  12672  smupval  12675  smueqlem  12677  smumullem  12679  gcdaddm  12704  bezoutlem1  12713  bezout  12717  gcddiv  12724  seq1st  12737  alginv  12741  algfx  12746  isprm2lem  12761  nn0gcdsq  12819  crt  12842  eulerthlem2  12846  pythagtriplem1  12865  iserodd  12884  pcqmul  12902  pcexp  12908  pcneg  12922  pcmpt  12936  pcfac  12943  prmreclem2  12960  prmreclem3  12961  1arith  12970  vdwpc  13023  ramcl  13072  imasval  13410  ercpbllem  13446  xpscfv  13460  iscat  13570  iscatd  13571  catideu  13573  iscatd2  13579  catlid  13581  catrid  13582  catass  13584  proplem  13588  homfeq  13593  comfeq  13605  catpropd  13608  moni  13635  epii  13642  sectffval  13649  sectfval  13650  oppcsect  13672  sectmon  13676  isfunc  13734  funcid  13740  funcco  13741  funcpropd  13770  isfull  13780  fthsect  13795  fthmon  13797  natfval  13816  isnat  13817  nati  13825  fucsect  13842  natpropd  13846  setcmon  13915  setcepi  13916  setcsect  13917  evlfcl  13992  uncfcurf  14009  yoniso  14055  isacs5lem  14268  acsdrscl  14269  acsficl  14270  latdisdlem  14288  latdisd  14289  isdlat  14292  dlatmjdi  14293  isps  14307  ismnd  14365  mgmidmo  14366  mndlem1  14367  mgmlrid  14385  ismndd  14392  mndpropd  14394  imasmnd2  14405  ismhm  14413  mhmpropd  14417  mhmlin  14418  mhmeql  14437  gsumvalx  14447  gsumval2  14456  gsumccat  14460  gsumwmhm  14463  frmdgsum  14480  isgrp  14489  grppropd  14496  isgrpd2e  14500  isgrpid2  14514  grpidd2  14515  grpinvfval  14516  grpinvpropd  14539  grpsubrcan  14543  grplactcnv  14560  mulgnn0p1  14574  mulgneg2  14590  mulgnnass  14591  mulgnn0ass  14592  mulgass  14593  mhmmulg  14595  imasgrp2  14606  isghm  14679  ghmlin  14684  ghmeql  14701  isga  14741  gagrpid  14744  gaass  14747  galcan  14754  orbsta  14763  cayleylem2  14784  cntzfval  14792  elcntz  14794  cntzsnval  14796  elcntzsn  14797  cntzi  14801  resscntz  14803  cntzmhm  14810  gsumwrev  14835  odfval  14844  mndodcong  14853  odbezout  14867  odeq1  14869  submod  14876  gexval  14885  gexdvds  14891  ispgp  14899  sylow1lem1  14905  sylow2alem1  14924  sylow2alem2  14925  sylow2blem2  14928  efgmnvl  15019  efgredlemc  15050  efgredeu  15057  frgpuptinv  15076  frgpup1  15080  frgpup3lem  15082  iscmn  15092  cmnpropd  15094  iscmnd  15097  abladdsub4  15111  submcmn2  15131  divsabl  15153  iscyg  15162  cygabl  15173  gsum2d  15219  dmdprd  15232  dprdval  15234  dprdfcntz  15246  subgdmdprd  15265  dprd2da  15273  dpjrid  15293  pgpfac1lem3a  15307  ablfaclem3  15318  ablfac2  15320  isrng  15341  rngpropd  15368  mulgass2  15383  imasrng  15398  dvdsr  15424  dvreq1  15471  isdrng  15512  drngprop  15519  isdrngd  15533  drngpropd  15535  isabv  15580  abvmul  15590  issrng  15611  issrngd  15622  islmod  15627  lmodlema  15628  islmodd  15629  lmodprop2d  15683  islmhm  15780  lmhmlin  15788  islmhm2  15791  lmhmeql  15808  lmhmpropd  15822  islbs  15825  lbspropd  15848  divscrng  15988  islpir  15997  rrgval  16024  unitrrg  16030  isassa  16052  assalem  16053  isassad  16059  assapropd  16063  mvrf1  16166  mplmonmul  16204  mplcoe1  16205  mplcoe3  16206  mplcoe2  16207  coe1tm  16345  ply1sclf1  16360  cnfldmulg  16402  cnfldexp  16403  prmirredlem  16442  chrcong  16479  zndvds  16499  znf1o  16501  znunit  16513  cygznlem3  16519  frgpcyg  16523  isphl  16528  ipcj  16534  iporthcom  16535  ip2eq  16553  isphld  16554  phlpropd  16555  ocvfval  16562  iscss  16579  ishil  16614  isobs  16616  obsip  16617  obslbs  16626  isperf  16878  restperf  16910  cmpsub  17123  iscon  17135  2ndcsep  17181  elptr2  17265  ptbasin  17268  dfac14  17308  txcnp  17310  ptcnplem  17311  ptcnp  17312  cnmpt11  17353  cnmpt21  17361  cnmptcom  17368  kqfeq  17411  isr0  17424  pt1hmeo  17493  imasdsf1olem  17933  isxms  17989  xmspropd  18015  imasf1oxms  18031  stdbdmopn  18060  isngp3  18116  ngppropd  18149  isnlm  18182  nmvs  18183  xrsxmet  18311  cnheibor  18449  htpyi  18468  htpycc  18474  pi1xfr  18549  pi1coghm  18555  isclm  18558  lmhmclm  18580  clmmulg  18587  iscph  18602  tchcph  18663  cmetcaulem  18710  bcth3  18749  ovolunlem1a  18851  ovolicc2lem1  18872  ovolicc2lem4  18875  ovolicc2  18877  mblsplit  18887  volun  18898  volfiniun  18900  voliunlem1  18903  volsup  18909  ioorinv  18927  uniioombllem2  18934  vitalilem3  18961  mbfeqalem  18993  mbflim  19019  itgeqa  19164  itgconst  19169  itgfsum  19177  itgsplitioo  19188  dvnadd  19274  dvnres  19276  dvexp  19298  dvmptfsum  19318  mvth  19335  dvlip  19336  lhop1lem  19356  dvcvx  19363  evlslem1  19395  mpfrcl  19398  evlsval  19399  mdegle0  19459  ply1nzb  19504  mon1pval  19523  facth1  19546  ig1pval  19554  dgrmulc  19648  dgrcolem1  19650  dgrcolem2  19651  dgrco  19652  coecj  19655  vieta1lem2  19687  vieta1  19688  elqaalem3  19697  dvntaylp  19746  ulmss  19770  mtest  19777  sineq0  19885  efif1olem4  19903  cxpexp  20011  mulcxplem  20027  mulcxp  20028  cxpmul2  20032  cxpeq  20093  affineequiv2  20120  quad2  20131  dcubic  20138  leibpi  20234  o1cxp  20265  scvxcvx  20276  wilthlem1  20302  wilthlem2  20303  perfect  20466  dchrelbas2  20472  dchrinv  20496  dchrptlem2  20500  lgsne0  20568  lgsqrlem2  20577  lgsdchr  20583  lgseisenlem2  20585  lgsquad2lem2  20594  dchrisumlem1  20634  qabvexp  20771  ostthlem1  20772  ostthlem2  20773  ostth3  20783  isgrpo  20857  grpoass  20864  grpoidinvlem3  20867  grpoidinv  20869  grpoideu  20870  grpoidinv2  20879  grpoinvfval  20885  isgrp2d  20896  gxcom  20930  gxinv  20931  gxnn0add  20935  gxnn0mul  20938  isablo  20944  ablocom  20946  gxdi  20957  issubgoilem  20970  isass  20977  opidon  20983  exidu1  20987  cmpidelt  20990  elghomlem2  21023  ghomlin  21025  ghgrplem2  21028  ghgrp  21029  ghablo  21030  isrngo  21039  rngoid  21044  rngoideu  21045  rngodi  21046  rngodir  21047  rngoass  21048  iscom2  21073  vci  21098  vcid  21101  vcdi  21102  vcdir  21103  vcass  21104  isvclem  21127  isnvlem  21160  nvmeq0  21216  nvs  21222  imsmetlem  21253  islno  21325  lnolin  21326  ishmo  21383  isphg  21389  phpar2  21395  phpar  21396  ipdiri  21402  ipasslem1  21403  ipasslem5  21407  ipasslem11  21412  ipassi  21413  dipdir  21414  dipass  21417  ip2eqi  21429  htth  21492  hvsubsub4  21635  hvnegdi  21642  hvaddcan  21645  hvaddcan2  21646  hvsubcan  21649  hvsubcan2  21650  hvaddsub4  21653  hial2eq  21681  normlem9at  21696  normsq  21709  norm-iii  21715  normsub  21718  normpyth  21720  normpar  21730  polid  21734  ococ  21981  chj0  22072  chlejb1  22087  chdmm1  22100  chjass  22108  spanun  22120  spansn  22134  elspansn2  22142  cmbr  22159  cmbr3  22183  pjoml2  22186  pjoml3  22187  osum  22220  spansnj  22222  pjch1  22245  pjadji  22260  pjaddi  22261  pjinormi  22262  pjsubi  22263  pjmuli  22264  pjcjt2  22267  pjch  22269  pjopyth  22295  pjpyth  22300  hoaddcom  22350  hoaddass  22358  hocsubdir  22361  hoaddid1  22367  ho0sub  22373  honegsub  22375  adjsym  22409  eigrei  22410  eigre  22411  eigposi  22412  eigorth  22414  ellnop  22434  elhmop  22449  ellnfn  22459  cnvadj  22468  lnopl  22490  unop  22491  hmop  22498  lnfnl  22507  adj1  22509  eleigvec  22533  hoddi  22566  lnopeq0lem2  22582  lnopunilem1  22586  lnopunilem2  22587  lnopunii  22588  elunop2  22589  lnophmi  22594  lnfnmul  22624  cnlnadjlem5  22647  branmfn  22681  bra11  22684  hmopidmchi  22727  hmopidmch  22729  hmopidmpj  22730  pjss2coi  22740  pjssmi  22741  pjssge0i  22742  pjidmco  22757  dfpjop  22758  elpjrn  22766  isst  22789  ishst  22790  hstel2  22795  stj  22811  mdbr  22870  mdi  22871  mdbr3  22873  dmdbr  22875  dmdmd  22876  dmdi  22878  dmdbr3  22881  mddmd2  22885  mdsl1i  22897  chjatom  22933  bcm1n  23028  subfacp1lem3  23120  subfacp1lem4  23121  subfacp1lem5  23122  subfacp1lem6  23123  subfacval2  23125  erdszelem9  23137  sconpht  23167  ptpcon  23171  cvmliftmolem1  23219  cvmliftmolem2  23220  cvmliftlem10  23232  cvmlift2  23254  cvmliftphtlem  23255  iseupa  23288  eupaseg  23295  eupap1  23307  eupath2  23311  ghomgrpilem1  23399  relexpsucr  23433  relexpsucl  23435  relexpcnv  23436  relexpadd  23442  sqdivzi  23485  mulcan2g  23491  fprb  23533  rdgprc  23555  dfrdg2  23556  preddowncl  23600  poseq  23657  soseq  23658  wfr3g  23659  wfrlem1  23660  wfrlem12  23671  wfrlem14  23673  wfrlem15  23674  wfr2  23677  wfr2c  23678  tfr3ALT  23683  frr3g  23684  frrlem1  23685  frrlem11  23697  sltval2  23713  sltres  23721  axfelem20  23769  fvsingle  23869  fullfunfv  23895  brcgr  23938  brbtwn2  23943  colinearalglem1  23944  colinearalg  23948  ax5seglem1  23966  ax5seglem2  23967  ax5seglem8  23974  ax5seglem9  23975  axlowdimlem13  23992  axlowdimlem16  23995  axlowdim1  23997  axcontlem1  24002  axcontlem2  24003  axcontlem6  24007  axcontlem7  24008  axcontlem8  24009  lineelsb2  24181  bpolyval  24194  bpolydif  24200  rankung  24206  ranksng  24207  rankpwg  24209  surjsec2  24531  repfuntw  24571  islatalg  24594  labss1  24600  labss2  24602  prodeq3ii  24719  iscom  24744  iscomb  24745  ridlideq  24746  smgrpass2  24752  fprodadd  24763  mndoass2  24771  fprodneg  24789  fprodsub  24790  trooo  24805  rltrooo  24826  com2i  24827  vecval1b  24862  vecval3b  24863  vecax5b  24870  glmrngo  24893  vecax5c  24894  vri  24903  cnegvex2  25071  rnegvex2  25072  cnegvex2b  25073  rnegvex2b  25074  addcanri  25077  addcanrg  25078  isded  25147  dedi  25148  1ded  25149  idosd  25155  domcmpd  25157  codcmpd  25158  iscatOLD  25165  cati  25166  1cat  25170  cmpasso  25184  cmpida  25185  cmpidb  25186  ismona  25220  ismonb  25221  idmon  25228  isepia  25230  isepib  25231  isiso  25236  cinvlem1  25239  cinvlem2  25240  isfuna  25245  isfunb  25246  issrc  25278  propsrc  25279  isntr  25284  cmp2morp  25369  rocatval  25370  cmppar3  25385  selsubf3g  25403  pgapspf2  25464  xsyysx  25556  opnregcld  25659  cldregopn  25660  neibastop3  25722  cocanfo  25785  upixp  25814  sdclem2  25863  caushft  25888  ismtycnv  25937  ismtyima  25938  ismtybndlem  25941  ismtyres  25943  bfplem2  25958  bfp  25959  grpoeqdivid  25982  ghomco  25984  rngohomval  26006  isrngohom  26007  rngohomadd  26011  rngohommul  26012  iscringd  26035  crngocom  26037  crngohomfo  26042  dmncan2  26113  fnelfp  26166  ismrcd2  26185  ismrc  26187  dvdsrabdioph  26302  fphpdo  26311  rmxypairf1o  26407  monotoddzzfi  26438  monotoddzz  26439  oddcomabszz  26440  rmxdioph  26520  expdiophlem2  26526  dnnumch3  26555  aomclem8  26570  islssfg  26579  unxpwdom3  26667  gicabl  26674  pmtrfrn  26811  cntzsdrg  26921  idomodle  26923  fgraphxp  26941  hausgraph  26942  caofcan  26951  expgrowth  26963  fmuldfeq  27124  climmulf  27141  climexp  27142  climsuse  27145  climrecf  27146  stoweidlem30  27190  stoweidlem48  27208  wallispilem4  27228  wallispi2lem1  27231  wallispi2lem2  27232  sbcfun  27376  csbafv12g  27391  csbaovg  27431  bnj1385  28144  bnj66  28171  bnj106  28179  bnj155  28190  bnj222  28194  bnj540  28203  bnj591  28222  bnj594  28223  bnj611  28229  bnj893  28239  bnj1000  28252  bnj966  28255  bnj1112  28292  bnj1234  28322  bnj1253  28326  bnj1280  28329  bnj1326  28335  bnj1450  28359  bnj1463  28364  bnj1529  28379  lshpset  28447  lcvexchlem4  28506  lcvexchlem5  28507  lflset  28528  islfl  28529  lfli  28530  islfld  28531  eqlkr3  28570  isopos  28649  oposlem  28652  opcon3b  28665  cmtvalN  28680  omllaw  28712  cvlexchb2  28800  cvlatexchb2  28804  cvlsupr2  28812  4atlem9  29071  4atlem10a  29072  4atlem11a  29075  4atlem12a  29078  4at2  29082  pmapglb2N  29239  pmapglb2xN  29240  paddasslem17  29304  ispsubclN  29405  ispsubcl2N  29415  lhpmod2i2  29506  lhpmod6i1  29507  4atexlemex2  29539  4atex  29544  4atex2-0aOLDN  29546  4atex2-0cOLDN  29548  ldilval  29581  ltrnfset  29585  ltrnset  29586  isltrn  29587  ltrneq2  29616  trnfsetN  29623  trnsetN  29624  istrnN  29625  cdlemd5  29670  cdleme0moN  29693  cdleme0nex  29758  cdleme18d  29763  cdleme31so  29847  cdleme31fv  29858  cdlemg2jlemOLDN  30061  cdlemg2fvlem  30062  cdlemg2klem  30063  istendo  30228  tendovalco  30233  tendoeq2  30242  dicelvalN  30647  dihval  30701  dihcnv11  30744  dihmeetlem13N  30788  dihlspsnat  30802  dochn0nv  30844  dochkrshp4  30858  lpolsetN  30951  lpolsatN  30957  lpolpolsatN  30958  lcfl1lem  30960  lclkrlem2a  30976  lclkrlem2e  30980  lcfls1lem  31003  lclkrs2  31009  lcdfval  31057  lcdval  31058  mapdffval  31095  mapdfval  31096  mapd0  31134  mapdpglem30  31171  mapdhval  31193  mapdheq2  31198  hdmap1vallem  31267  hdmap1val  31268  hdmap1cbv  31272  hdmapval3N  31310  hdmap10  31312  hdmapeq0  31316  hdmap14lem12  31351  hdmap14lem13  31352  hgmapfval  31358  hgmapvs  31363  hgmapvv  31398  hlhilocv  31429
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 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2277
  Copyright terms: Public domain W3C validator