Theorem eqeq12d 2211

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 2209	. 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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  cdeqeq  2984  sbceqg  3100  csbing  3370  uniprg  3854  unisng  3856  intprg  3907  iununir  4000  csbopabg  4111  undifexmid  4226  exmidundif  4239  exmidundifim  4240  limeq  4412  onsucuni2  4600  ordpwsucexmid  4606  csbima12g  5030  dmsnsnsng  5147  cnvsng  5155  csbiotag  5251  fvmptf  5654  eqfnfv2f  5663  fvreseq  5665  fmptco  5728  fnressn  5748  fvsng  5758  cocan1  5834  cocan2  5835  fliftfun  5843  csbriotag  5890  oveqrspc2v  5949  csbov123g  5960  eqfnov  6029  ovmpos  6046  ov2gf  6047  ovmpodxf  6048  caovcomg  6079  caovassg  6082  caovcang  6085  caovcanrd  6087  caovcan  6088  caovdig  6098  caovdirg  6101  caovimo  6117  offveqb  6155  op1stg  6208  op2ndg  6209  f1o2ndf1  6286  tfrlem1  6366  tfrlem3ag  6367  tfrlem3a  6368  tfrlem5  6372  tfrlem9  6377  tfr0dm  6380  tfrlemiubacc  6388  tfrlemiex  6389  tfrlemi1  6390  tfr1onlem3ag  6395  tfr1onlemubacc  6404  tfr1onlemex  6405  tfr1onlemaccex  6406  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemubacc  6417  tfrcllemex  6418  tfrcllemaccex  6419  tfrcllemres  6420  tfrcldm  6421  tfri3  6425  rdg0g  6446  frecrdg  6466  nna0r  6536  nnacom  6542  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  nnmcom  6547  ecopovtrn  6691  ecopovsymg  6693  ecopovtrng  6694  ecovcom  6701  ecovicom  6702  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  dom2lem  6831  ordiso2  7101  inl11  7131  updjud  7148  omp1eomlem  7160  difinfsnlem  7165  nnnninfeq  7194  nninfwlporlemd  7238  nninfwlpor  7240  exmidfodomrlemrALT  7270  exmidaclem  7275  addcanpig  7401  mulcanpig  7402  mulcmpblnq  7435  mulpipqqs  7440  ordpipqqs  7441  mulidnq  7456  enq0sym  7499  nqnq0  7508  mulcmpblnq0  7511  distrnq0  7526  mulcomnq0  7527  addassnq0  7529  nq02m  7532  genipv  7576  cauappcvgprlemladd  7725  addcmpblnr  7806  0idsr  7834  1idsr  7835  axaddcom  7937  ax1rid  7944  ax0id  7945  rereceu  7956  axcaucvg  7967  mulrid  8023  readdcan  8166  cnegexlem1  8201  cnegexlem3  8203  addcan  8206  addcan2  8207  apti  8649  mulcanapd  8688  mulcanap2d  8689  div11ap  8727  divmuleqap  8744  conjmulap  8756  eqneg  8759  cnref1o  9725  fzsuc2  10154  fzprval  10157  fztpval  10158  qtri3or  10330  modqadd1  10453  modqmul1  10469  addmodlteq  10490  frec2uzrdg  10501  frecuzrdgg  10508  seq3val  10552  seqvalcd  10553  seq3fveq2  10567  seqfveq2g  10569  seqfveqg  10570  seq3fveq  10571  seq3feq  10572  seq3shft2  10573  seqshft2g  10574  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3caopr2  10585  seqcaopr2g  10586  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemqk  10599  seq3f1olemqsum  10605  seq3f1olemstep  10606  seq3f1olemp  10607  seq3f1oleml  10608  seqf1oglem2a  10610  seqf1oglem2  10612  seqf1og  10613  seq3id  10617  seq3id2  10618  seq3homo  10619  seqhomog  10622  seqfeq4g  10623  mulexp  10670  expadd  10673  expmul  10676  modqexp  10758  nn0opth2d  10815  bcpasc  10858  hashennn  10872  hashen  10876  omgadd  10894  hashfzo  10914  hashfzp1  10916  hashxp  10918  hashfacen  10928  seq3coll  10934  shftvalg  11001  shftval4g  11002  replim  11024  cjreb  11031  cjexp  11058  absexp  11244  recan  11274  minclpr  11402  mingeb  11407  sumeq2  11524  zsumdc  11549  fsum3  11552  fsumf1o  11555  fsum3cvg2  11559  fsumadd  11571  isummulc2  11591  fsum2d  11600  fsummulc2  11613  fsumconst  11619  modfsummod  11623  fsumparts  11635  fsumrelem  11636  fsumiun  11642  binom  11649  bcxmas  11654  isumshft  11655  isumnn0nn  11658  mertenslem2  11701  clim2prod  11704  prodfrecap  11711  prodeq2  11722  zproddc  11744  fprodseq  11748  fprodf1o  11753  prodsnf  11757  fprodfac  11780  fprodabs  11781  fprodconst  11785  fprod2d  11788  fprodrec  11794  fprodmodd  11806  efne0  11843  efexp  11847  demoivreALT  11939  moddvds  11964  gcddiv  12186  alginv  12215  algfx  12220  lcmneg  12242  lcmid  12248  lcmgcdeq  12251  divgcdcoprm0  12269  cncongr1  12271  cncongr2  12272  nn0gcdsq  12368  crth  12392  eulerthlema  12398  eulerthlemh  12399  pythagtriplem1  12434  pcqmul  12472  pcexp  12478  pcneg  12494  pcmpt  12512  pcfac  12519  1arith  12536  setscomd  12719  ercpbllemg  12973  mgmidmo  13015  mgmlrid  13022  lidrideqd  13024  lidrididd  13025  grpinvalem  13028  grpinva  13029  issgrp  13046  isnsgrp  13049  sgrpass  13051  sgrp1  13054  issgrpd  13055  sgrppropd  13056  ismndd  13078  mndpropd  13081  mnd1  13087  mnd1id  13088  ismhm  13093  mhmpropd  13098  mhmlin  13099  mhmeql  13124  isgrp  13138  grppropd  13149  isgrpd2e  13152  dfgrp2  13159  isgrpid2  13172  grpidd2  13173  grpinvfvalg  13174  grpinvpropdg  13207  grpidssd  13208  grpinvssd  13209  grpsubrcan  13213  dfgrp3mlem  13230  grplactcnv  13234  imasgrp2  13240  mhmlem  13244  mulgnn0p1  13263  mulgaddcom  13276  mulginvcom  13277  mulgneg2  13286  mulgnnass  13287  mulgnn0ass  13288  mulgass  13289  mhmmulg  13293  isghm  13373  ghmlin  13378  ghmeql  13397  iscmn  13423  cmnpropd  13425  iscmnd  13428  abladdsub4  13444  imasabl  13466  gsumfzconst  13471  isrng  13490  rngass  13495  rngdi  13496  rngdir  13497  rngpropd  13511  imasrng  13512  issrg  13521  srgmulgass  13545  srgpcomp  13546  srg1expzeq1  13551  isring  13556  iscrng2  13571  ringpropd  13594  ringinvnz1ne0  13605  mulgass2  13614  ring1  13615  imasring  13620  opprnegg  13639  dvdsrd  13650  dvreq1  13698  rhmmul  13720  isrhm2d  13721  rhmopp  13732  rhmunitinv  13734  islring  13748  rrgval  13818  unitrrg  13823  opprdomnbg  13830  islmod  13847  lmodlema  13848  islmodd  13849  lmodvsmmulgdi  13879  lmodprop2d  13904  rmodislmodlem  13906  rmodislmod  13907  rnglidlmsgrp  14053  rnglidlrng  14054  quscrng  14089  cnfldmulg  14132  cnfldexp  14133  gsumfzfsumlemm  14143  zndvds  14205  znf1o  14207  znunit  14215  txcnp  14507  cnmpt11  14519  cnmpt21  14527  cnmptcom  14534  isxms  14687  xmspropd  14713  bdmopn  14740  dvexp  14947  dvmptfsum  14961  rpcxpmul2  15149  wilthlem1  15216  mpodvdsmulf1o  15226  fsumdvdsmul  15227  perfect  15237  lgsne0  15279  gausslemma2d  15310  lgseisenlem2  15312  lgsquad2lem2  15323  2lgslem1a  15329  2lgslem1b  15330  nninffeq  15664