Theorem eqeq12d 2253

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

Step	Hyp	Ref	Expression
1		eqeq12d.1	. 2 |- ( ph -> A = B )
2		eqeq12d.2	. 2 |- ( ph -> C = D )
3		eqeq12 2251	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A = C <-> B = D ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3950  unisng  3952  intprg  4003  iununir  4096  csbopabg  4210  undifexmid  4332  exmidundif  4345  exmidundifim  4346  limeq  4524  onsucuni2  4713  ordpwsucexmid  4719  csbima12g  5151  dmsnsnsng  5268  cnvsng  5276  csbiotag  5373  fvmptf  5801  eqfnfv2f  5813  fvreseq  5815  fmptco  5877  fnressn  5904  fvsng  5914  cocan1  5996  cocan2  5997  fliftfun  6005  csbriotag  6055  oveqrspc2v  6115  csbov123g  6127  eqfnov  6198  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  caovcomg  6248  caovassg  6251  caovcang  6254  caovcanrd  6256  caovcan  6257  caovdig  6267  caovdirg  6270  caovimo  6286  offveqb  6326  caofid0l  6333  caofid0r  6334  op1stg  6388  op2ndg  6389  f1o2ndf1  6468  tfrlem1  6583  tfrlem3ag  6584  tfrlem3a  6585  tfrlem5  6589  tfrlem9  6594  tfr0dm  6597  tfrlemiubacc  6605  tfrlemiex  6606  tfrlemi1  6607  tfr1onlem3ag  6612  tfr1onlemubacc  6621  tfr1onlemex  6622  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemubacc  6634  tfrcllemex  6635  tfrcllemaccex  6636  tfrcllemres  6637  tfrcldm  6638  tfri3  6642  rdg0g  6663  frecrdg  6683  nna0r  6755  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  ecopovtrn  6910  ecopovsymg  6912  ecopovtrng  6913  ecovcom  6920  ecovicom  6921  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  dom2lem  7062  ordiso2  7381  inl11  7411  updjud  7428  omp1eomlem  7440  difinfsnlem  7445  nnnninfeq  7474  nninfwlporlemd  7518  nninfwlpor  7520  nninfinfwlpo  7526  exmidfodomrlemrALT  7561  exmidaclem  7570  addcanpig  7707  mulcanpig  7708  mulcmpblnq  7741  mulpipqqs  7746  ordpipqqs  7747  mulidnq  7762  enq0sym  7805  nqnq0  7814  mulcmpblnq0  7817  distrnq0  7832  mulcomnq0  7833  addassnq0  7835  nq02m  7838  genipv  7882  cauappcvgprlemladd  8031  addcmpblnr  8112  0idsr  8140  1idsr  8141  axaddcom  8243  ax1rid  8250  ax0id  8251  rereceu  8262  axcaucvg  8273  mulrid  8329  readdcan  8473  cnegexlem1  8508  cnegexlem3  8510  addcan  8513  addcan2  8514  apti  8958  mulcanapd  8997  mulcanap2d  8998  div11ap  9038  divmuleqap  9055  conjmulap  9067  eqneg  9070  ofsubeq0  9300  cnref1o  10068  fzsuc2  10503  fzprval  10506  fztpval  10507  qtri3or  10692  modqadd1  10819  modqmul1  10835  addmodlteq  10856  frec2uzrdg  10867  frecuzrdgg  10874  seq3val  10918  seqvalcd  10919  seq3fveq2  10933  seqfveq2g  10935  seqfveqg  10936  seq3fveq  10937  seq3feq  10938  seq3shft2  10939  seqshft2g  10940  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seq3caopr2  10951  seqcaopr2g  10952  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqk  10965  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1olemp  10973  seq3f1oleml  10974  seqf1oglem2a  10976  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3id2  10984  seq3homo  10985  seqhomog  10988  seqfeq4g  10989  mulexp  11036  expadd  11039  expmul  11042  modqexp  11125  nn0opth2d  11183  bcpasc  11226  bcm1n  11229  hashennn  11241  hashen  11245  omgadd  11264  hashfzo  11285  hashfzp1  11287  hashxp  11289  hashmap  11290  hashfibclem  11304  hashfibc  11305  hashfacen  11306  hashf1lem1  11307  hashf1lem2  11308  hashf1  11309  seq3coll  11316  eqs1  11418  swrdspsleq  11461  pfxeq  11490  pfxsuff1eqwrdeq  11493  ccatopth2  11511  cats1un  11515  swrdccatin1  11519  swrdccat3blem  11533  shftvalg  11623  shftval4g  11624  replim  11646  cjreb  11653  cjexp  11680  absexp  11868  recan  11898  minclpr  12027  mingeb  12033  sumeq2  12150  zsumdc  12176  fsum3  12179  fsumf1o  12182  fsum3cvg2  12186  fsumadd  12198  isummulc2  12218  fsum2d  12227  fsummulc2  12240  fsumconst  12246  modfsummod  12250  fsumparts  12262  fsumrelem  12263  fsumiun  12269  binom  12276  bcxmas  12281  isumshft  12282  isumnn0nn  12285  mertenslem2  12328  clim2prod  12331  prodfrecap  12338  prodeq2  12349  zproddc  12371  fprodseq  12375  fprodf1o  12380  prodsnf  12384  fprodfac  12407  fprodabs  12408  fprodconst  12412  fprod2d  12415  fprodrec  12421  fprodmodd  12433  efne0  12470  efexp  12474  demoivreALT  12566  moddvds  12591  bitsinv1  12754  gcddiv  12821  alginv  12850  algfx  12855  lcmneg  12877  lcmid  12883  lcmgcdeq  12886  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  nn0gcdsq  13005  crth  13031  eulerthlema  13037  eulerthlemh  13038  pythagtriplem1  13073  pcqmul  13111  pcexp  13117  pcneg  13133  pcmpt  13151  pcfac  13158  1arith  13175  setscomd  13451  ercpbllemg  13710  mgmidmo  13751  mgmlrid  13758  lidrideqd  13760  lidrididd  13761  grpinvalem  13764  grpinva  13765  issgrp  13777  isnsgrp  13780  sgrpass  13782  sgrp1  13785  issgrpd  13786  sgrppropd  13787  ismndd  13809  mndpropd  13812  imasmnd2  13818  mnd1  13821  mnd1id  13822  ismhm  13827  mhmpropd  13832  mhmlin  13833  mhmeql  13858  isgrp  13870  grppropd  13881  isgrpd2e  13884  dfgrp2  13891  isgrpid2  13904  grpidd2  13905  grpinvfvalg  13906  grpinvpropdg  13939  grpidssd  13940  grpinvssd  13941  grpsubrcan  13945  dfgrp3mlem  13962  grplactcnv  13966  imasgrp2  13972  mhmlem  13976  mulgnn0p1  13995  mulgaddcom  14008  mulginvcom  14009  mulgneg2  14018  mulgnnass  14019  mulgnn0ass  14020  mulgass  14021  mhmmulg  14025  isghm  14105  ghmlin  14110  ghmeql  14129  cntzex  14150  cntzfval  14152  elcntz  14154  cntzsnval  14156  elcntzsn  14157  cntzi  14162  resscntz  14166  cntzmhm  14173  iscmn  14186  cmnpropd  14188  iscmnd  14191  cmnsubm  14202  abladdsub4  14208  imasabl  14230  gzsumconst  14233  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  gsumconstcmn  14266  gsum2dfilem2  14272  isrng  14340  rngass  14345  rngdi  14346  rngdir  14347  rngpropd  14361  imasrng  14362  issrg  14376  srgmulgass  14400  srgpcomp  14401  srg1expzeq1  14406  isring  14411  iscrng2  14426  ringpropd  14450  ringinvnz1ne0  14461  mulgass2  14470  ring1  14471  imasring  14478  opprnegg  14498  dvdsrd  14510  dvreq1  14558  rhmmul  14580  isrhm2d  14581  rhmopp  14592  rhmunitinv  14594  islring  14608  opprlring  14613  rrgval  14679  unitrrg  14685  opprdomnbg  14692  islmod  14736  lmodlema  14737  islmodd  14738  lmodvsmmulgdi  14769  lmodprop2d  14794  rmodislmodlem  14796  rmodislmod  14797  rnglidlmsgrp  14943  rnglidlrng  14944  quscrng  14979  cnfldmulg  15022  cnfldexp  15023  gsumfsum  15032  zndvds  15093  znf1o  15095  znunit  15103  isassa  15111  assalem  15112  isassad  15120  assapropd  15123  assamulgscm  15152  psr1clfi  15198  txcnp  15497  cnmpt11  15509  cnmpt21  15517  cnmptcom  15524  isxms  15677  xmspropd  15703  bdmopn  15730  dvexp  15937  dvmptfsum  15951  sineq0re  16076  rpcxpmul2  16146  wilthlem1  16232  mpodvdsmulf1o  16284  fsumdvdsmul  16285  perfect  16301  lgsne0  16362  gausslemma2d  16393  lgseisenlem2  16395  lgsquad2lem2  16406  2lgslem1a  16412  2lgslem1b  16413  usgredg2v  16670  issubgr  16703  wkslem1  16766  wkslem2  16767  iswlk  16769  uspgr2wlkeq  16811  2wlklem  16822  wlkres  16825  eupth2lem3fi  16922  eupth2fi  16925  depindlem1  16952  depindlem2  16953  depindlem3  16954  depind  16955  nninffeq  17269