Theorem eqeq12d 2154

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  cdeqeq  2904  sbceqg  3018  csbing  3283  uniprg  3751  unisng  3753  intprg  3804  iununir  3896  csbopabg  4006  undifexmid  4117  exmidundif  4129  exmidundifim  4130  limeq  4299  onsucuni2  4479  ordpwsucexmid  4485  csbima12g  4900  dmsnsnsng  5016  cnvsng  5024  csbiotag  5116  fvmptf  5513  eqfnfv2f  5522  fvreseq  5524  fmptco  5586  fnressn  5606  fvsng  5616  cocan1  5688  cocan2  5689  fliftfun  5697  csbriotag  5742  csbov123g  5809  eqfnov  5877  ovmpos  5894  ov2gf  5895  ovmpodxf  5896  caovcomg  5926  caovassg  5929  caovcang  5932  caovcanrd  5934  caovcan  5935  caovdig  5945  caovdirg  5948  caovimo  5964  grprinvlem  5965  grprinvd  5966  offveqb  6001  op1stg  6048  op2ndg  6049  f1o2ndf1  6125  tfrlem1  6205  tfrlem3ag  6206  tfrlem3a  6207  tfrlem5  6211  tfrlem9  6216  tfr0dm  6219  tfrlemiubacc  6227  tfrlemiex  6228  tfrlemi1  6229  tfr1onlem3ag  6234  tfr1onlemubacc  6243  tfr1onlemex  6244  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemubacc  6256  tfrcllemex  6257  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  tfri3  6264  rdg0g  6285  frecrdg  6305  nna0r  6374  nnacom  6380  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  ecopovtrn  6526  ecopovsymg  6528  ecopovtrng  6529  ecovcom  6536  ecovicom  6537  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  dom2lem  6666  ordiso2  6920  inl11  6950  updjud  6967  omp1eomlem  6979  difinfsnlem  6984  exmidfodomrlemrALT  7059  exmidaclem  7064  addcanpig  7142  mulcanpig  7143  mulcmpblnq  7176  mulpipqqs  7181  ordpipqqs  7182  mulidnq  7197  enq0sym  7240  nqnq0  7249  mulcmpblnq0  7252  distrnq0  7267  mulcomnq0  7268  addassnq0  7270  nq02m  7273  genipv  7317  cauappcvgprlemladd  7466  addcmpblnr  7547  0idsr  7575  1idsr  7576  axaddcom  7678  ax1rid  7685  ax0id  7686  rereceu  7697  axcaucvg  7708  mulid1  7763  readdcan  7902  cnegexlem1  7937  cnegexlem3  7939  addcan  7942  addcan2  7943  apti  8384  mulcanapd  8422  mulcanap2d  8423  div11ap  8460  divmuleqap  8477  conjmulap  8489  eqneg  8492  cnref1o  9440  fzsuc2  9859  fzprval  9862  fztpval  9863  qtri3or  10020  modqadd1  10134  modqmul1  10150  addmodlteq  10171  frec2uzrdg  10182  frecuzrdgg  10189  seq3val  10231  seqvalcd  10232  seq3fveq2  10242  seq3fveq  10244  seq3feq  10245  seq3shft2  10246  seq3split  10252  seq3caopr3  10254  seq3caopr2  10255  iseqf1olemkle  10257  iseqf1olemklt  10258  iseqf1olemqk  10267  seq3f1olemqsum  10273  seq3f1olemstep  10274  seq3f1olemp  10275  seq3f1oleml  10276  seq3id  10281  seq3id2  10282  seq3homo  10283  mulexp  10332  expadd  10335  expmul  10338  nn0opth2d  10469  bcpasc  10512  hashennn  10526  hashen  10530  omgadd  10548  hashfzo  10568  hashfzp1  10570  hashxp  10572  hashfacen  10579  seq3coll  10585  shftvalg  10608  shftval4g  10609  replim  10631  cjreb  10638  cjexp  10665  absexp  10851  recan  10881  minclpr  11008  sumeq2  11128  zsumdc  11153  fsum3  11156  fsumf1o  11159  fsum3cvg2  11163  fsumadd  11175  isummulc2  11195  fsum2d  11204  fsummulc2  11217  fsumconst  11223  modfsummod  11227  fsumparts  11239  fsumrelem  11240  fsumiun  11246  binom  11253  bcxmas  11258  isumshft  11259  isumnn0nn  11262  mertenslem2  11305  clim2prod  11308  prodfrecap  11315  prodeq2  11326  efne0  11384  efexp  11388  demoivreALT  11480  moddvds  11502  gcddiv  11707  alginv  11728  algfx  11733  lcmneg  11755  lcmid  11761  lcmgcdeq  11764  divgcdcoprm0  11782  cncongr1  11784  cncongr2  11785  nn0gcdsq  11878  crth  11900  txcnp  12440  cnmpt11  12452  cnmpt21  12460  cnmptcom  12467  isxms  12620  xmspropd  12646  bdmopn  12673  dvexp  12844  nninfalllemn  13202  nninffeq  13216