Theorem eqeq12d 2249

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 2247	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A = C <-> B = D ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227

This theorem is referenced by:  cdeqeq  3040  sbceqg  3157  csbing  3432  uniprg  3934  unisng  3936  intprg  3987  iununir  4080  csbopabg  4193  undifexmid  4311  exmidundif  4324  exmidundifim  4325  limeq  4503  onsucuni2  4691  ordpwsucexmid  4697  csbima12g  5128  dmsnsnsng  5245  cnvsng  5253  csbiotag  5350  fvmptf  5775  eqfnfv2f  5784  fvreseq  5786  fmptco  5848  fnressn  5875  fvsng  5885  cocan1  5966  cocan2  5967  fliftfun  5975  csbriotag  6025  oveqrspc2v  6085  csbov123g  6097  eqfnov  6168  ovmpos  6185  ov2gf  6186  ovmpodxf  6187  caovcomg  6218  caovassg  6221  caovcang  6224  caovcanrd  6226  caovcan  6227  caovdig  6237  caovdirg  6240  caovimo  6256  offveqb  6295  caofid0l  6302  caofid0r  6303  op1stg  6357  op2ndg  6358  f1o2ndf1  6437  tfrlem1  6552  tfrlem3ag  6553  tfrlem3a  6554  tfrlem5  6558  tfrlem9  6563  tfr0dm  6566  tfrlemiubacc  6574  tfrlemiex  6575  tfrlemi1  6576  tfr1onlem3ag  6581  tfr1onlemubacc  6590  tfr1onlemex  6591  tfr1onlemaccex  6592  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemubacc  6603  tfrcllemex  6604  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  tfri3  6611  rdg0g  6632  frecrdg  6652  nna0r  6724  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  ecopovtrn  6879  ecopovsymg  6881  ecopovtrng  6882  ecovcom  6889  ecovicom  6890  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  dom2lem  7024  ordiso2  7339  inl11  7369  updjud  7386  omp1eomlem  7398  difinfsnlem  7403  nnnninfeq  7432  nninfwlporlemd  7476  nninfwlpor  7478  nninfinfwlpo  7484  exmidfodomrlemrALT  7519  exmidaclem  7528  addcanpig  7665  mulcanpig  7666  mulcmpblnq  7699  mulpipqqs  7704  ordpipqqs  7705  mulidnq  7720  enq0sym  7763  nqnq0  7772  mulcmpblnq0  7775  distrnq0  7790  mulcomnq0  7791  addassnq0  7793  nq02m  7796  genipv  7840  cauappcvgprlemladd  7989  addcmpblnr  8070  0idsr  8098  1idsr  8099  axaddcom  8201  ax1rid  8208  ax0id  8209  rereceu  8220  axcaucvg  8231  mulrid  8287  readdcan  8429  cnegexlem1  8464  cnegexlem3  8466  addcan  8469  addcan2  8470  apti  8913  mulcanapd  8952  mulcanap2d  8953  div11ap  8991  divmuleqap  9008  conjmulap  9020  eqneg  9023  cnref1o  10001  fzsuc2  10435  fzprval  10438  fztpval  10439  qtri3or  10624  modqadd1  10747  modqmul1  10763  addmodlteq  10784  frec2uzrdg  10795  frecuzrdgg  10802  seq3val  10846  seqvalcd  10847  seq3fveq2  10861  seqfveq2g  10863  seqfveqg  10864  seq3fveq  10865  seq3feq  10866  seq3shft2  10867  seqshft2g  10868  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seq3caopr2  10879  seqcaopr2g  10880  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqk  10893  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1olemp  10901  seq3f1oleml  10902  seqf1oglem2a  10904  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3id2  10912  seq3homo  10913  seqhomog  10916  seqfeq4g  10917  mulexp  10964  expadd  10967  expmul  10970  modqexp  11053  nn0opth2d  11110  bcpasc  11153  bcm1n  11156  hashennn  11168  hashen  11172  omgadd  11191  hashfzo  11212  hashfzp1  11214  hashxp  11216  hashmap  11217  hashfibclem  11231  hashfibc  11232  hashfacen  11233  seq3coll  11239  eqs1  11341  swrdspsleq  11384  pfxeq  11413  pfxsuff1eqwrdeq  11416  ccatopth2  11434  cats1un  11438  swrdccatin1  11442  swrdccat3blem  11456  shftvalg  11546  shftval4g  11547  replim  11569  cjreb  11576  cjexp  11603  absexp  11789  recan  11819  minclpr  11947  mingeb  11952  sumeq2  12069  zsumdc  12095  fsum3  12098  fsumf1o  12101  fsum3cvg2  12105  fsumadd  12117  isummulc2  12137  fsum2d  12146  fsummulc2  12159  fsumconst  12165  modfsummod  12169  fsumparts  12181  fsumrelem  12182  fsumiun  12188  binom  12195  bcxmas  12200  isumshft  12201  isumnn0nn  12204  mertenslem2  12247  clim2prod  12250  prodfrecap  12257  prodeq2  12268  zproddc  12290  fprodseq  12294  fprodf1o  12299  prodsnf  12303  fprodfac  12326  fprodabs  12327  fprodconst  12331  fprod2d  12334  fprodrec  12340  fprodmodd  12352  efne0  12389  efexp  12393  demoivreALT  12485  moddvds  12510  bitsinv1  12673  gcddiv  12740  alginv  12769  algfx  12774  lcmneg  12796  lcmid  12802  lcmgcdeq  12805  divgcdcoprm0  12823  cncongr1  12825  cncongr2  12826  nn0gcdsq  12922  crth  12946  eulerthlema  12952  eulerthlemh  12953  pythagtriplem1  12988  pcqmul  13026  pcexp  13032  pcneg  13048  pcmpt  13066  pcfac  13073  1arith  13090  setscomd  13337  ercpbllemg  13594  mgmidmo  13635  mgmlrid  13642  lidrideqd  13644  lidrididd  13645  grpinvalem  13648  grpinva  13649  issgrp  13666  isnsgrp  13669  sgrpass  13671  sgrp1  13674  issgrpd  13675  sgrppropd  13676  ismndd  13698  mndpropd  13701  imasmnd2  13707  mnd1  13710  mnd1id  13711  ismhm  13716  mhmpropd  13721  mhmlin  13722  mhmeql  13747  isgrp  13761  grppropd  13772  isgrpd2e  13775  dfgrp2  13782  isgrpid2  13795  grpidd2  13796  grpinvfvalg  13797  grpinvpropdg  13830  grpidssd  13831  grpinvssd  13832  grpsubrcan  13836  dfgrp3mlem  13853  grplactcnv  13857  imasgrp2  13863  mhmlem  13867  mulgnn0p1  13886  mulgaddcom  13899  mulginvcom  13900  mulgneg2  13909  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  mhmmulg  13916  isghm  13996  ghmlin  14001  ghmeql  14020  iscmn  14046  cmnpropd  14048  iscmnd  14051  abladdsub4  14067  imasabl  14089  gsumfzconst  14094  isrng  14173  rngass  14178  rngdi  14179  rngdir  14180  rngpropd  14194  imasrng  14195  issrg  14208  srgmulgass  14232  srgpcomp  14233  srg1expzeq1  14238  isring  14243  iscrng2  14258  ringpropd  14281  ringinvnz1ne0  14292  mulgass2  14301  ring1  14302  imasring  14307  opprnegg  14327  dvdsrd  14339  dvreq1  14387  rhmmul  14409  isrhm2d  14410  rhmopp  14421  rhmunitinv  14423  islring  14437  opprlring  14442  rrgval  14508  unitrrg  14514  opprdomnbg  14521  islmod  14565  lmodlema  14566  islmodd  14567  lmodvsmmulgdi  14597  lmodprop2d  14622  rmodislmodlem  14624  rmodislmod  14625  rnglidlmsgrp  14771  rnglidlrng  14772  quscrng  14807  cnfldmulg  14850  cnfldexp  14851  gsumfzfsumlemm  14861  zndvds  14923  znf1o  14925  znunit  14933  psr1clfi  14969  txcnp  15262  cnmpt11  15274  cnmpt21  15282  cnmptcom  15289  isxms  15442  xmspropd  15468  bdmopn  15495  dvexp  15702  dvmptfsum  15716  rpcxpmul2  15904  wilthlem1  15974  mpodvdsmulf1o  15984  fsumdvdsmul  15985  perfect  15995  lgsne0  16037  gausslemma2d  16068  lgseisenlem2  16070  lgsquad2lem2  16081  2lgslem1a  16087  2lgslem1b  16088  usgredg2v  16345  issubgr  16378  wkslem1  16441  wkslem2  16442  iswlk  16444  uspgr2wlkeq  16486  2wlklem  16497  wlkres  16500  eupth2lem3fi  16597  eupth2fi  16600  depindlem1  16627  depindlem2  16628  depindlem3  16629  depind  16630  nninffeq  16924