Theorem eqeq12d 2192

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 2190	. 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 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  cdeqeq  2957  sbceqg  3073  csbing  3342  uniprg  3823  unisng  3825  intprg  3876  iununir  3968  csbopabg  4079  undifexmid  4191  exmidundif  4204  exmidundifim  4205  limeq  4375  onsucuni2  4561  ordpwsucexmid  4567  csbima12g  4986  dmsnsnsng  5103  cnvsng  5111  csbiotag  5206  fvmptf  5605  eqfnfv2f  5614  fvreseq  5616  fmptco  5679  fnressn  5699  fvsng  5709  cocan1  5783  cocan2  5784  fliftfun  5792  csbriotag  5838  oveqrspc2v  5897  csbov123g  5908  eqfnov  5976  ovmpos  5993  ov2gf  5994  ovmpodxf  5995  caovcomg  6025  caovassg  6028  caovcang  6031  caovcanrd  6033  caovcan  6034  caovdig  6044  caovdirg  6047  caovimo  6063  offveqb  6097  op1stg  6146  op2ndg  6147  f1o2ndf1  6224  tfrlem1  6304  tfrlem3ag  6305  tfrlem3a  6306  tfrlem5  6310  tfrlem9  6315  tfr0dm  6318  tfrlemiubacc  6326  tfrlemiex  6327  tfrlemi1  6328  tfr1onlem3ag  6333  tfr1onlemubacc  6342  tfr1onlemex  6343  tfr1onlemaccex  6344  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllemubacc  6355  tfrcllemex  6356  tfrcllemaccex  6357  tfrcllemres  6358  tfrcldm  6359  tfri3  6363  rdg0g  6384  frecrdg  6404  nna0r  6474  nnacom  6480  nnaass  6481  nndi  6482  nnmass  6483  nnmsucr  6484  nnmcom  6485  ecopovtrn  6627  ecopovsymg  6629  ecopovtrng  6630  ecovcom  6637  ecovicom  6638  ecovass  6639  ecoviass  6640  ecovdi  6641  ecovidi  6642  dom2lem  6767  ordiso2  7029  inl11  7059  updjud  7076  omp1eomlem  7088  difinfsnlem  7093  nnnninfeq  7121  nninfwlporlemd  7165  nninfwlpor  7167  exmidfodomrlemrALT  7197  exmidaclem  7202  addcanpig  7328  mulcanpig  7329  mulcmpblnq  7362  mulpipqqs  7367  ordpipqqs  7368  mulidnq  7383  enq0sym  7426  nqnq0  7435  mulcmpblnq0  7438  distrnq0  7453  mulcomnq0  7454  addassnq0  7456  nq02m  7459  genipv  7503  cauappcvgprlemladd  7652  addcmpblnr  7733  0idsr  7761  1idsr  7762  axaddcom  7864  ax1rid  7871  ax0id  7872  rereceu  7883  axcaucvg  7894  mulrid  7949  readdcan  8091  cnegexlem1  8126  cnegexlem3  8128  addcan  8131  addcan2  8132  apti  8573  mulcanapd  8612  mulcanap2d  8613  div11ap  8651  divmuleqap  8668  conjmulap  8680  eqneg  8683  cnref1o  9644  fzsuc2  10072  fzprval  10075  fztpval  10076  qtri3or  10236  modqadd1  10354  modqmul1  10370  addmodlteq  10391  frec2uzrdg  10402  frecuzrdgg  10409  seq3val  10451  seqvalcd  10452  seq3fveq2  10462  seq3fveq  10464  seq3feq  10465  seq3shft2  10466  seq3split  10472  seq3caopr3  10474  seq3caopr2  10475  iseqf1olemkle  10477  iseqf1olemklt  10478  iseqf1olemqk  10487  seq3f1olemqsum  10493  seq3f1olemstep  10494  seq3f1olemp  10495  seq3f1oleml  10496  seq3id  10501  seq3id2  10502  seq3homo  10503  mulexp  10552  expadd  10555  expmul  10558  modqexp  10639  nn0opth2d  10694  bcpasc  10737  hashennn  10751  hashen  10755  omgadd  10773  hashfzo  10793  hashfzp1  10795  hashxp  10797  hashfacen  10807  seq3coll  10813  shftvalg  10836  shftval4g  10837  replim  10859  cjreb  10866  cjexp  10893  absexp  11079  recan  11109  minclpr  11236  mingeb  11241  sumeq2  11358  zsumdc  11383  fsum3  11386  fsumf1o  11389  fsum3cvg2  11393  fsumadd  11405  isummulc2  11425  fsum2d  11434  fsummulc2  11447  fsumconst  11453  modfsummod  11457  fsumparts  11469  fsumrelem  11470  fsumiun  11476  binom  11483  bcxmas  11488  isumshft  11489  isumnn0nn  11492  mertenslem2  11535  clim2prod  11538  prodfrecap  11545  prodeq2  11556  zproddc  11578  fprodseq  11582  fprodf1o  11587  prodsnf  11591  fprodfac  11614  fprodabs  11615  fprodconst  11619  fprod2d  11622  fprodrec  11628  fprodmodd  11640  efne0  11677  efexp  11681  demoivreALT  11772  moddvds  11797  gcddiv  12010  alginv  12037  algfx  12042  lcmneg  12064  lcmid  12070  lcmgcdeq  12073  divgcdcoprm0  12091  cncongr1  12093  cncongr2  12094  nn0gcdsq  12190  crth  12214  eulerthlema  12220  eulerthlemh  12221  pythagtriplem1  12255  pcqmul  12293  pcexp  12299  pcneg  12314  pcmpt  12331  pcfac  12338  1arith  12355  setscomd  12493  mgmidmo  12721  mgmlrid  12728  lidrideqd  12730  lidrididd  12731  grprinvlem  12734  grprinvd  12735  issgrp  12739  isnsgrp  12742  sgrpass  12744  sgrp1  12746  ismndd  12768  mndpropd  12771  mnd1  12775  mnd1id  12776  ismhm  12781  mhmpropd  12785  mhmlin  12786  mhmeql  12804  isgrp  12811  grppropd  12821  isgrpd2e  12824  dfgrp2  12830  isgrpid2  12841  grpidd2  12842  grpinvfvalg  12843  grpinvpropdg  12873  grpidssd  12874  grpinvssd  12875  grpsubrcan  12879  dfgrp3mlem  12896  grplactcnv  12900  mhmlem  12906  mulgnn0p1  12922  mulgaddcom  12934  mulginvcom  12935  mulgneg2  12944  mulgnnass  12945  mulgnn0ass  12946  mulgass  12947  mhmmulg  12951  iscmn  12996  cmnpropd  12998  iscmnd  13001  abladdsub4  13017  issrg  13048  srgmulgass  13072  srgpcomp  13073  srg1expzeq1  13078  isring  13083  iscrng2  13098  ringpropd  13117  ringinvnz1ne0  13126  mulgass2  13135  ring1  13136  opprnegg  13152  dvdsrd  13162  dvreq1  13210  islring  13232  cnfldmulg  13275  cnfldexp  13276  txcnp  13553  cnmpt11  13565  cnmpt21  13573  cnmptcom  13580  isxms  13733  xmspropd  13759  bdmopn  13786  dvexp  13957  lgsne0  14221  nninffeq  14540