Theorem eqeq12d 2204

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 2202	. 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 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  cdeqeq  2972  sbceqg  3088  csbing  3357  uniprg  3839  unisng  3841  intprg  3892  iununir  3985  csbopabg  4096  undifexmid  4211  exmidundif  4224  exmidundifim  4225  limeq  4395  onsucuni2  4581  ordpwsucexmid  4587  csbima12g  5007  dmsnsnsng  5124  cnvsng  5132  csbiotag  5228  fvmptf  5629  eqfnfv2f  5638  fvreseq  5640  fmptco  5703  fnressn  5723  fvsng  5733  cocan1  5809  cocan2  5810  fliftfun  5818  csbriotag  5865  oveqrspc2v  5924  csbov123g  5935  eqfnov  6004  ovmpos  6021  ov2gf  6022  ovmpodxf  6023  caovcomg  6053  caovassg  6056  caovcang  6059  caovcanrd  6061  caovcan  6062  caovdig  6072  caovdirg  6075  caovimo  6091  offveqb  6127  op1stg  6176  op2ndg  6177  f1o2ndf1  6254  tfrlem1  6334  tfrlem3ag  6335  tfrlem3a  6336  tfrlem5  6340  tfrlem9  6345  tfr0dm  6348  tfrlemiubacc  6356  tfrlemiex  6357  tfrlemi1  6358  tfr1onlem3ag  6363  tfr1onlemubacc  6372  tfr1onlemex  6373  tfr1onlemaccex  6374  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllemubacc  6385  tfrcllemex  6386  tfrcllemaccex  6387  tfrcllemres  6388  tfrcldm  6389  tfri3  6393  rdg0g  6414  frecrdg  6434  nna0r  6504  nnacom  6510  nnaass  6511  nndi  6512  nnmass  6513  nnmsucr  6514  nnmcom  6515  ecopovtrn  6659  ecopovsymg  6661  ecopovtrng  6662  ecovcom  6669  ecovicom  6670  ecovass  6671  ecoviass  6672  ecovdi  6673  ecovidi  6674  dom2lem  6799  ordiso2  7065  inl11  7095  updjud  7112  omp1eomlem  7124  difinfsnlem  7129  nnnninfeq  7157  nninfwlporlemd  7201  nninfwlpor  7203  exmidfodomrlemrALT  7233  exmidaclem  7238  addcanpig  7364  mulcanpig  7365  mulcmpblnq  7398  mulpipqqs  7403  ordpipqqs  7404  mulidnq  7419  enq0sym  7462  nqnq0  7471  mulcmpblnq0  7474  distrnq0  7489  mulcomnq0  7490  addassnq0  7492  nq02m  7495  genipv  7539  cauappcvgprlemladd  7688  addcmpblnr  7769  0idsr  7797  1idsr  7798  axaddcom  7900  ax1rid  7907  ax0id  7908  rereceu  7919  axcaucvg  7930  mulrid  7985  readdcan  8128  cnegexlem1  8163  cnegexlem3  8165  addcan  8168  addcan2  8169  apti  8610  mulcanapd  8649  mulcanap2d  8650  div11ap  8688  divmuleqap  8705  conjmulap  8717  eqneg  8720  cnref1o  9682  fzsuc2  10111  fzprval  10114  fztpval  10115  qtri3or  10275  modqadd1  10394  modqmul1  10410  addmodlteq  10431  frec2uzrdg  10442  frecuzrdgg  10449  seq3val  10491  seqvalcd  10492  seq3fveq2  10502  seq3fveq  10504  seq3feq  10505  seq3shft2  10506  seq3split  10512  seq3caopr3  10514  seq3caopr2  10515  iseqf1olemkle  10517  iseqf1olemklt  10518  iseqf1olemqk  10527  seq3f1olemqsum  10533  seq3f1olemstep  10534  seq3f1olemp  10535  seq3f1oleml  10536  seq3id  10541  seq3id2  10542  seq3homo  10543  seqfeq4g  10546  mulexp  10593  expadd  10596  expmul  10599  modqexp  10681  nn0opth2d  10738  bcpasc  10781  hashennn  10795  hashen  10799  omgadd  10817  hashfzo  10837  hashfzp1  10839  hashxp  10841  hashfacen  10851  seq3coll  10857  shftvalg  10880  shftval4g  10881  replim  10903  cjreb  10910  cjexp  10937  absexp  11123  recan  11153  minclpr  11280  mingeb  11285  sumeq2  11402  zsumdc  11427  fsum3  11430  fsumf1o  11433  fsum3cvg2  11437  fsumadd  11449  isummulc2  11469  fsum2d  11478  fsummulc2  11491  fsumconst  11497  modfsummod  11501  fsumparts  11513  fsumrelem  11514  fsumiun  11520  binom  11527  bcxmas  11532  isumshft  11533  isumnn0nn  11536  mertenslem2  11579  clim2prod  11582  prodfrecap  11589  prodeq2  11600  zproddc  11622  fprodseq  11626  fprodf1o  11631  prodsnf  11635  fprodfac  11658  fprodabs  11659  fprodconst  11663  fprod2d  11666  fprodrec  11672  fprodmodd  11684  efne0  11721  efexp  11725  demoivreALT  11816  moddvds  11841  gcddiv  12055  alginv  12082  algfx  12087  lcmneg  12109  lcmid  12115  lcmgcdeq  12118  divgcdcoprm0  12136  cncongr1  12138  cncongr2  12139  nn0gcdsq  12235  crth  12259  eulerthlema  12265  eulerthlemh  12266  pythagtriplem1  12300  pcqmul  12338  pcexp  12344  pcneg  12360  pcmpt  12378  pcfac  12385  1arith  12402  setscomd  12556  ercpbllemg  12809  mgmidmo  12851  mgmlrid  12858  lidrideqd  12860  lidrididd  12861  grpinvalem  12864  grpinva  12865  issgrp  12881  isnsgrp  12884  sgrpass  12886  sgrp1  12889  issgrpd  12890  sgrppropd  12891  ismndd  12913  mndpropd  12916  mnd1  12922  mnd1id  12923  ismhm  12928  mhmpropd  12933  mhmlin  12934  mhmeql  12959  isgrp  12966  grppropd  12977  isgrpd2e  12980  dfgrp2  12986  isgrpid2  12999  grpidd2  13000  grpinvfvalg  13001  grpinvpropdg  13034  grpidssd  13035  grpinvssd  13036  grpsubrcan  13040  dfgrp3mlem  13057  grplactcnv  13061  imasgrp2  13067  mhmlem  13071  mulgnn0p1  13090  mulgaddcom  13103  mulginvcom  13104  mulgneg2  13113  mulgnnass  13114  mulgnn0ass  13115  mulgass  13116  mhmmulg  13120  isghm  13199  ghmlin  13204  ghmeql  13223  iscmn  13249  cmnpropd  13251  iscmnd  13254  abladdsub4  13270  imasabl  13290  isrng  13305  rngass  13310  rngdi  13311  rngdir  13312  rngpropd  13326  imasrng  13327  issrg  13336  srgmulgass  13360  srgpcomp  13361  srg1expzeq1  13366  isring  13371  iscrng2  13386  ringpropd  13409  ringinvnz1ne0  13418  mulgass2  13427  ring1  13428  imasring  13431  opprnegg  13450  dvdsrd  13461  dvreq1  13509  rhmmul  13531  isrhm2d  13532  rhmopp  13543  rhmunitinv  13545  islring  13556  islmod  13624  lmodlema  13625  islmodd  13626  lmodvsmmulgdi  13656  lmodprop2d  13681  rmodislmodlem  13683  rmodislmod  13684  rnglidlmsgrp  13830  rnglidlrng  13831  quscrng  13864  cnfldmulg  13896  cnfldexp  13897  txcnp  14248  cnmpt11  14260  cnmpt21  14268  cnmptcom  14275  isxms  14428  xmspropd  14454  bdmopn  14481  dvexp  14652  wilthlem1  14875  lgsne0  14917  lgseisenlem2  14929  nninffeq  15248