Theorem eqeq12d 2180

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  cdeqeq  2945  sbceqg  3060  csbing  3328  uniprg  3803  unisng  3805  intprg  3856  iununir  3948  csbopabg  4059  undifexmid  4171  exmidundif  4184  exmidundifim  4185  limeq  4354  onsucuni2  4540  ordpwsucexmid  4546  csbima12g  4964  dmsnsnsng  5080  cnvsng  5088  csbiotag  5180  fvmptf  5577  eqfnfv2f  5586  fvreseq  5588  fmptco  5650  fnressn  5670  fvsng  5680  cocan1  5754  cocan2  5755  fliftfun  5763  csbriotag  5809  csbov123g  5876  eqfnov  5944  ovmpos  5961  ov2gf  5962  ovmpodxf  5963  caovcomg  5993  caovassg  5996  caovcang  5999  caovcanrd  6001  caovcan  6002  caovdig  6012  caovdirg  6015  caovimo  6031  grprinvlem  6032  grprinvd  6033  offveqb  6068  op1stg  6115  op2ndg  6116  f1o2ndf1  6192  tfrlem1  6272  tfrlem3ag  6273  tfrlem3a  6274  tfrlem5  6278  tfrlem9  6283  tfr0dm  6286  tfrlemiubacc  6294  tfrlemiex  6295  tfrlemi1  6296  tfr1onlem3ag  6301  tfr1onlemubacc  6310  tfr1onlemex  6311  tfr1onlemaccex  6312  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemubacc  6323  tfrcllemex  6324  tfrcllemaccex  6325  tfrcllemres  6326  tfrcldm  6327  tfri3  6331  rdg0g  6352  frecrdg  6372  nna0r  6442  nnacom  6448  nnaass  6449  nndi  6450  nnmass  6451  nnmsucr  6452  nnmcom  6453  ecopovtrn  6594  ecopovsymg  6596  ecopovtrng  6597  ecovcom  6604  ecovicom  6605  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  dom2lem  6734  ordiso2  6996  inl11  7026  updjud  7043  omp1eomlem  7055  difinfsnlem  7060  nnnninfeq  7088  exmidfodomrlemrALT  7155  exmidaclem  7160  addcanpig  7271  mulcanpig  7272  mulcmpblnq  7305  mulpipqqs  7310  ordpipqqs  7311  mulidnq  7326  enq0sym  7369  nqnq0  7378  mulcmpblnq0  7381  distrnq0  7396  mulcomnq0  7397  addassnq0  7399  nq02m  7402  genipv  7446  cauappcvgprlemladd  7595  addcmpblnr  7676  0idsr  7704  1idsr  7705  axaddcom  7807  ax1rid  7814  ax0id  7815  rereceu  7826  axcaucvg  7837  mulid1  7892  readdcan  8034  cnegexlem1  8069  cnegexlem3  8071  addcan  8074  addcan2  8075  apti  8516  mulcanapd  8554  mulcanap2d  8555  div11ap  8592  divmuleqap  8609  conjmulap  8621  eqneg  8624  cnref1o  9584  fzsuc2  10010  fzprval  10013  fztpval  10014  qtri3or  10174  modqadd1  10292  modqmul1  10308  addmodlteq  10329  frec2uzrdg  10340  frecuzrdgg  10347  seq3val  10389  seqvalcd  10390  seq3fveq2  10400  seq3fveq  10402  seq3feq  10403  seq3shft2  10404  seq3split  10410  seq3caopr3  10412  seq3caopr2  10413  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqk  10425  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1olemp  10433  seq3f1oleml  10434  seq3id  10439  seq3id2  10440  seq3homo  10441  mulexp  10490  expadd  10493  expmul  10496  modqexp  10577  nn0opth2d  10632  bcpasc  10675  hashennn  10689  hashen  10693  omgadd  10711  hashfzo  10731  hashfzp1  10733  hashxp  10735  hashfacen  10745  seq3coll  10751  shftvalg  10774  shftval4g  10775  replim  10797  cjreb  10804  cjexp  10831  absexp  11017  recan  11047  minclpr  11174  mingeb  11179  sumeq2  11296  zsumdc  11321  fsum3  11324  fsumf1o  11327  fsum3cvg2  11331  fsumadd  11343  isummulc2  11363  fsum2d  11372  fsummulc2  11385  fsumconst  11391  modfsummod  11395  fsumparts  11407  fsumrelem  11408  fsumiun  11414  binom  11421  bcxmas  11426  isumshft  11427  isumnn0nn  11430  mertenslem2  11473  clim2prod  11476  prodfrecap  11483  prodeq2  11494  zproddc  11516  fprodseq  11520  fprodf1o  11525  prodsnf  11529  fprodfac  11552  fprodabs  11553  fprodconst  11557  fprod2d  11560  fprodrec  11566  fprodmodd  11578  efne0  11615  efexp  11619  demoivreALT  11710  moddvds  11735  gcddiv  11948  alginv  11975  algfx  11980  lcmneg  12002  lcmid  12008  lcmgcdeq  12011  divgcdcoprm0  12029  cncongr1  12031  cncongr2  12032  nn0gcdsq  12128  crth  12152  eulerthlema  12158  eulerthlemh  12159  pythagtriplem1  12193  pcqmul  12231  pcexp  12237  pcneg  12252  pcmpt  12269  pcfac  12276  1arith  12293  txcnp  12871  cnmpt11  12883  cnmpt21  12891  cnmptcom  12898  isxms  13051  xmspropd  13077  bdmopn  13104  dvexp  13275  lgsne0  13539  nninffeq  13860