Theorem eqeq12d 2247

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 2245	. 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 2214

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

This theorem is referenced by:  cdeqeq  3037  sbceqg  3154  csbing  3428  uniprg  3929  unisng  3931  intprg  3982  iununir  4075  csbopabg  4188  undifexmid  4306  exmidundif  4319  exmidundifim  4320  limeq  4498  onsucuni2  4686  ordpwsucexmid  4692  csbima12g  5123  dmsnsnsng  5240  cnvsng  5248  csbiotag  5345  fvmptf  5770  eqfnfv2f  5779  fvreseq  5781  fmptco  5843  fnressn  5870  fvsng  5880  cocan1  5960  cocan2  5961  fliftfun  5969  csbriotag  6017  oveqrspc2v  6077  csbov123g  6089  eqfnov  6160  ovmpos  6177  ov2gf  6178  ovmpodxf  6179  caovcomg  6210  caovassg  6213  caovcang  6216  caovcanrd  6218  caovcan  6219  caovdig  6229  caovdirg  6232  caovimo  6248  offveqb  6286  caofid0l  6293  caofid0r  6294  op1stg  6344  op2ndg  6345  f1o2ndf1  6424  tfrlem1  6539  tfrlem3ag  6540  tfrlem3a  6541  tfrlem5  6545  tfrlem9  6550  tfr0dm  6553  tfrlemiubacc  6561  tfrlemiex  6562  tfrlemi1  6563  tfr1onlem3ag  6568  tfr1onlemubacc  6577  tfr1onlemex  6578  tfr1onlemaccex  6579  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemubacc  6590  tfrcllemex  6591  tfrcllemaccex  6592  tfrcllemres  6593  tfrcldm  6594  tfri3  6598  rdg0g  6619  frecrdg  6639  nna0r  6711  nnacom  6717  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  nnmcom  6722  ecopovtrn  6866  ecopovsymg  6868  ecopovtrng  6869  ecovcom  6876  ecovicom  6877  ecovass  6878  ecoviass  6879  ecovdi  6880  ecovidi  6881  dom2lem  7011  ordiso2  7326  inl11  7356  updjud  7373  omp1eomlem  7385  difinfsnlem  7390  nnnninfeq  7419  nninfwlporlemd  7463  nninfwlpor  7465  nninfinfwlpo  7471  exmidfodomrlemrALT  7506  exmidaclem  7515  addcanpig  7649  mulcanpig  7650  mulcmpblnq  7683  mulpipqqs  7688  ordpipqqs  7689  mulidnq  7704  enq0sym  7747  nqnq0  7756  mulcmpblnq0  7759  distrnq0  7774  mulcomnq0  7775  addassnq0  7777  nq02m  7780  genipv  7824  cauappcvgprlemladd  7973  addcmpblnr  8054  0idsr  8082  1idsr  8083  axaddcom  8185  ax1rid  8192  ax0id  8193  rereceu  8204  axcaucvg  8215  mulrid  8271  readdcan  8413  cnegexlem1  8448  cnegexlem3  8450  addcan  8453  addcan2  8454  apti  8896  mulcanapd  8935  mulcanap2d  8936  div11ap  8974  divmuleqap  8991  conjmulap  9003  eqneg  9006  cnref1o  9983  fzsuc2  10413  fzprval  10416  fztpval  10417  qtri3or  10600  modqadd1  10723  modqmul1  10739  addmodlteq  10760  frec2uzrdg  10771  frecuzrdgg  10778  seq3val  10822  seqvalcd  10823  seq3fveq2  10837  seqfveq2g  10839  seqfveqg  10840  seq3fveq  10841  seq3feq  10842  seq3shft2  10843  seqshft2g  10844  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seq3caopr2  10855  seqcaopr2g  10856  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqk  10869  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1olemp  10877  seq3f1oleml  10878  seqf1oglem2a  10880  seqf1oglem2  10882  seqf1og  10883  seq3id  10887  seq3id2  10888  seq3homo  10889  seqhomog  10892  seqfeq4g  10893  mulexp  10940  expadd  10943  expmul  10946  modqexp  11028  nn0opth2d  11085  bcpasc  11128  bcm1n  11131  hashennn  11143  hashen  11147  omgadd  11166  hashfzo  11187  hashfzp1  11189  hashxp  11191  hashmap  11192  hashfibclem  11206  hashfibc  11207  hashfacen  11208  seq3coll  11214  eqs1  11316  swrdspsleq  11359  pfxeq  11388  pfxsuff1eqwrdeq  11391  ccatopth2  11409  cats1un  11413  swrdccatin1  11417  swrdccat3blem  11431  shftvalg  11521  shftval4g  11522  replim  11544  cjreb  11551  cjexp  11578  absexp  11764  recan  11794  minclpr  11922  mingeb  11927  sumeq2  12044  zsumdc  12070  fsum3  12073  fsumf1o  12076  fsum3cvg2  12080  fsumadd  12092  isummulc2  12112  fsum2d  12121  fsummulc2  12134  fsumconst  12140  modfsummod  12144  fsumparts  12156  fsumrelem  12157  fsumiun  12163  binom  12170  bcxmas  12175  isumshft  12176  isumnn0nn  12179  mertenslem2  12222  clim2prod  12225  prodfrecap  12232  prodeq2  12243  zproddc  12265  fprodseq  12269  fprodf1o  12274  prodsnf  12278  fprodfac  12301  fprodabs  12302  fprodconst  12306  fprod2d  12309  fprodrec  12315  fprodmodd  12327  efne0  12364  efexp  12368  demoivreALT  12460  moddvds  12485  bitsinv1  12648  gcddiv  12715  alginv  12744  algfx  12749  lcmneg  12771  lcmid  12777  lcmgcdeq  12780  divgcdcoprm0  12798  cncongr1  12800  cncongr2  12801  nn0gcdsq  12897  crth  12921  eulerthlema  12927  eulerthlemh  12928  pythagtriplem1  12963  pcqmul  13001  pcexp  13007  pcneg  13023  pcmpt  13041  pcfac  13048  1arith  13065  setscomd  13253  ercpbllemg  13543  mgmidmo  13585  mgmlrid  13592  lidrideqd  13594  lidrididd  13595  grpinvalem  13598  grpinva  13599  issgrp  13616  isnsgrp  13619  sgrpass  13621  sgrp1  13624  issgrpd  13625  sgrppropd  13626  ismndd  13650  mndpropd  13653  imasmnd2  13665  mnd1  13668  mnd1id  13669  ismhm  13674  mhmpropd  13679  mhmlin  13680  mhmeql  13705  isgrp  13719  grppropd  13730  isgrpd2e  13733  dfgrp2  13740  isgrpid2  13753  grpidd2  13754  grpinvfvalg  13755  grpinvpropdg  13788  grpidssd  13789  grpinvssd  13790  grpsubrcan  13794  dfgrp3mlem  13811  grplactcnv  13815  imasgrp2  13827  mhmlem  13831  mulgnn0p1  13850  mulgaddcom  13863  mulginvcom  13864  mulgneg2  13873  mulgnnass  13874  mulgnn0ass  13875  mulgass  13876  mhmmulg  13880  isghm  13960  ghmlin  13965  ghmeql  13984  iscmn  14010  cmnpropd  14012  iscmnd  14015  abladdsub4  14031  imasabl  14053  gsumfzconst  14058  isrng  14078  rngass  14083  rngdi  14084  rngdir  14085  rngpropd  14099  imasrng  14100  issrg  14109  srgmulgass  14133  srgpcomp  14134  srg1expzeq1  14139  isring  14144  iscrng2  14159  ringpropd  14182  ringinvnz1ne0  14193  mulgass2  14202  ring1  14203  imasring  14208  opprnegg  14227  dvdsrd  14239  dvreq1  14287  rhmmul  14309  isrhm2d  14310  rhmopp  14321  rhmunitinv  14323  islring  14337  rrgval  14407  unitrrg  14413  opprdomnbg  14420  islmod  14439  lmodlema  14440  islmodd  14441  lmodvsmmulgdi  14471  lmodprop2d  14496  rmodislmodlem  14498  rmodislmod  14499  rnglidlmsgrp  14645  rnglidlrng  14646  quscrng  14681  cnfldmulg  14724  cnfldexp  14725  gsumfzfsumlemm  14735  zndvds  14797  znf1o  14799  znunit  14807  psr1clfi  14843  txcnp  15136  cnmpt11  15148  cnmpt21  15156  cnmptcom  15163  isxms  15316  xmspropd  15342  bdmopn  15369  dvexp  15576  dvmptfsum  15590  rpcxpmul2  15778  wilthlem1  15848  mpodvdsmulf1o  15858  fsumdvdsmul  15859  perfect  15869  lgsne0  15911  gausslemma2d  15942  lgseisenlem2  15944  lgsquad2lem2  15955  2lgslem1a  15961  2lgslem1b  15962  usgredg2v  16219  issubgr  16252  wkslem1  16315  wkslem2  16316  iswlk  16318  uspgr2wlkeq  16360  2wlklem  16371  wlkres  16374  eupth2lem3fi  16471  eupth2fi  16474  depindlem1  16501  depindlem2  16502  depindlem3  16503  depind  16504  nninffeq  16798