Theorem eqeq12d 2172

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 2170	. 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 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  cdeqeq  2932  sbceqg  3047  csbing  3314  uniprg  3787  unisng  3789  intprg  3840  iununir  3932  csbopabg  4042  undifexmid  4153  exmidundif  4166  exmidundifim  4167  limeq  4336  onsucuni2  4521  ordpwsucexmid  4527  csbima12g  4944  dmsnsnsng  5060  cnvsng  5068  csbiotag  5160  fvmptf  5557  eqfnfv2f  5566  fvreseq  5568  fmptco  5630  fnressn  5650  fvsng  5660  cocan1  5732  cocan2  5733  fliftfun  5741  csbriotag  5786  csbov123g  5853  eqfnov  5921  ovmpos  5938  ov2gf  5939  ovmpodxf  5940  caovcomg  5970  caovassg  5973  caovcang  5976  caovcanrd  5978  caovcan  5979  caovdig  5989  caovdirg  5992  caovimo  6008  grprinvlem  6009  grprinvd  6010  offveqb  6045  op1stg  6092  op2ndg  6093  f1o2ndf1  6169  tfrlem1  6249  tfrlem3ag  6250  tfrlem3a  6251  tfrlem5  6255  tfrlem9  6260  tfr0dm  6263  tfrlemiubacc  6271  tfrlemiex  6272  tfrlemi1  6273  tfr1onlem3ag  6278  tfr1onlemubacc  6287  tfr1onlemex  6288  tfr1onlemaccex  6289  tfrcllemsucaccv  6295  tfrcllembxssdm  6297  tfrcllemubacc  6300  tfrcllemex  6301  tfrcllemaccex  6302  tfrcllemres  6303  tfrcldm  6304  tfri3  6308  rdg0g  6329  frecrdg  6349  nna0r  6418  nnacom  6424  nnaass  6425  nndi  6426  nnmass  6427  nnmsucr  6428  nnmcom  6429  ecopovtrn  6570  ecopovsymg  6572  ecopovtrng  6573  ecovcom  6580  ecovicom  6581  ecovass  6582  ecoviass  6583  ecovdi  6584  ecovidi  6585  dom2lem  6710  ordiso2  6969  inl11  6999  updjud  7016  omp1eomlem  7028  difinfsnlem  7033  exmidfodomrlemrALT  7121  exmidaclem  7126  addcanpig  7237  mulcanpig  7238  mulcmpblnq  7271  mulpipqqs  7276  ordpipqqs  7277  mulidnq  7292  enq0sym  7335  nqnq0  7344  mulcmpblnq0  7347  distrnq0  7362  mulcomnq0  7363  addassnq0  7365  nq02m  7368  genipv  7412  cauappcvgprlemladd  7561  addcmpblnr  7642  0idsr  7670  1idsr  7671  axaddcom  7773  ax1rid  7780  ax0id  7781  rereceu  7792  axcaucvg  7803  mulid1  7858  readdcan  7998  cnegexlem1  8033  cnegexlem3  8035  addcan  8038  addcan2  8039  apti  8480  mulcanapd  8518  mulcanap2d  8519  div11ap  8556  divmuleqap  8573  conjmulap  8585  eqneg  8588  cnref1o  9541  fzsuc2  9963  fzprval  9966  fztpval  9967  qtri3or  10124  modqadd1  10242  modqmul1  10258  addmodlteq  10279  frec2uzrdg  10290  frecuzrdgg  10297  seq3val  10339  seqvalcd  10340  seq3fveq2  10350  seq3fveq  10352  seq3feq  10353  seq3shft2  10354  seq3split  10360  seq3caopr3  10362  seq3caopr2  10363  iseqf1olemkle  10365  iseqf1olemklt  10366  iseqf1olemqk  10375  seq3f1olemqsum  10381  seq3f1olemstep  10382  seq3f1olemp  10383  seq3f1oleml  10384  seq3id  10389  seq3id2  10390  seq3homo  10391  mulexp  10440  expadd  10443  expmul  10446  modqexp  10526  nn0opth2d  10579  bcpasc  10622  hashennn  10636  hashen  10640  omgadd  10658  hashfzo  10678  hashfzp1  10680  hashxp  10682  hashfacen  10689  seq3coll  10695  shftvalg  10718  shftval4g  10719  replim  10741  cjreb  10748  cjexp  10775  absexp  10961  recan  10991  minclpr  11118  sumeq2  11238  zsumdc  11263  fsum3  11266  fsumf1o  11269  fsum3cvg2  11273  fsumadd  11285  isummulc2  11305  fsum2d  11314  fsummulc2  11327  fsumconst  11333  modfsummod  11337  fsumparts  11349  fsumrelem  11350  fsumiun  11356  binom  11363  bcxmas  11368  isumshft  11369  isumnn0nn  11372  mertenslem2  11415  clim2prod  11418  prodfrecap  11425  prodeq2  11436  zproddc  11458  fprodseq  11462  fprodf1o  11467  prodsnf  11471  fprodfac  11494  fprodabs  11495  fprodconst  11499  fprod2d  11502  fprodrec  11508  fprodmodd  11520  efne0  11557  efexp  11561  demoivreALT  11652  moddvds  11677  gcddiv  11883  alginv  11904  algfx  11909  lcmneg  11931  lcmid  11937  lcmgcdeq  11940  divgcdcoprm0  11958  cncongr1  11960  cncongr2  11961  nn0gcdsq  12054  crth  12076  eulerthlema  12082  eulerthlemh  12083  txcnp  12631  cnmpt11  12643  cnmpt21  12651  cnmptcom  12658  isxms  12811  xmspropd  12837  bdmopn  12864  dvexp  13035  nninfalllemn  13541  nninffeq  13554