Theorem eqeq12d 2253

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3945  unisng  3947  intprg  3998  iununir  4091  csbopabg  4204  undifexmid  4325  exmidundif  4338  exmidundifim  4339  limeq  4517  onsucuni2  4706  ordpwsucexmid  4712  csbima12g  5143  dmsnsnsng  5260  cnvsng  5268  csbiotag  5365  fvmptf  5792  eqfnfv2f  5801  fvreseq  5803  fmptco  5865  fnressn  5892  fvsng  5902  cocan1  5983  cocan2  5984  fliftfun  5992  csbriotag  6042  oveqrspc2v  6102  csbov123g  6114  eqfnov  6185  ovmpos  6202  ov2gf  6203  ovmpodxf  6204  caovcomg  6235  caovassg  6238  caovcang  6241  caovcanrd  6243  caovcan  6244  caovdig  6254  caovdirg  6257  caovimo  6273  offveqb  6312  caofid0l  6319  caofid0r  6320  op1stg  6374  op2ndg  6375  f1o2ndf1  6454  tfrlem1  6569  tfrlem3ag  6570  tfrlem3a  6571  tfrlem5  6575  tfrlem9  6580  tfr0dm  6583  tfrlemiubacc  6591  tfrlemiex  6592  tfrlemi1  6593  tfr1onlem3ag  6598  tfr1onlemubacc  6607  tfr1onlemex  6608  tfr1onlemaccex  6609  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemubacc  6620  tfrcllemex  6621  tfrcllemaccex  6622  tfrcllemres  6623  tfrcldm  6624  tfri3  6628  rdg0g  6649  frecrdg  6669  nna0r  6741  nnacom  6747  nnaass  6748  nndi  6749  nnmass  6750  nnmsucr  6751  nnmcom  6752  ecopovtrn  6896  ecopovsymg  6898  ecopovtrng  6899  ecovcom  6906  ecovicom  6907  ecovass  6908  ecoviass  6909  ecovdi  6910  ecovidi  6911  dom2lem  7048  ordiso2  7365  inl11  7395  updjud  7412  omp1eomlem  7424  difinfsnlem  7429  nnnninfeq  7458  nninfwlporlemd  7502  nninfwlpor  7504  nninfinfwlpo  7510  exmidfodomrlemrALT  7545  exmidaclem  7554  addcanpig  7691  mulcanpig  7692  mulcmpblnq  7725  mulpipqqs  7730  ordpipqqs  7731  mulidnq  7746  enq0sym  7789  nqnq0  7798  mulcmpblnq0  7801  distrnq0  7816  mulcomnq0  7817  addassnq0  7819  nq02m  7822  genipv  7866  cauappcvgprlemladd  8015  addcmpblnr  8096  0idsr  8124  1idsr  8125  axaddcom  8227  ax1rid  8234  ax0id  8235  rereceu  8246  axcaucvg  8257  mulrid  8313  readdcan  8456  cnegexlem1  8491  cnegexlem3  8493  addcan  8496  addcan2  8497  apti  8940  mulcanapd  8979  mulcanap2d  8980  div11ap  9020  divmuleqap  9037  conjmulap  9049  eqneg  9052  cnref1o  10030  fzsuc2  10464  fzprval  10467  fztpval  10468  qtri3or  10653  modqadd1  10776  modqmul1  10792  addmodlteq  10813  frec2uzrdg  10824  frecuzrdgg  10831  seq3val  10875  seqvalcd  10876  seq3fveq2  10890  seqfveq2g  10892  seqfveqg  10893  seq3fveq  10894  seq3feq  10895  seq3shft2  10896  seqshft2g  10897  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seq3caopr2  10908  seqcaopr2g  10909  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemqk  10922  seq3f1olemqsum  10928  seq3f1olemstep  10929  seq3f1olemp  10930  seq3f1oleml  10931  seqf1oglem2a  10933  seqf1oglem2  10935  seqf1og  10936  seq3id  10940  seq3id2  10941  seq3homo  10942  seqhomog  10945  seqfeq4g  10946  mulexp  10993  expadd  10996  expmul  10999  modqexp  11082  nn0opth2d  11139  bcpasc  11182  bcm1n  11185  hashennn  11197  hashen  11201  omgadd  11220  hashfzo  11241  hashfzp1  11243  hashxp  11245  hashmap  11246  hashfibclem  11260  hashfibc  11261  hashfacen  11262  hashf1lem1  11263  hashf1lem2  11264  hashf1  11265  seq3coll  11272  eqs1  11374  swrdspsleq  11417  pfxeq  11446  pfxsuff1eqwrdeq  11449  ccatopth2  11467  cats1un  11471  swrdccatin1  11475  swrdccat3blem  11489  shftvalg  11579  shftval4g  11580  replim  11602  cjreb  11609  cjexp  11636  absexp  11823  recan  11853  minclpr  11981  mingeb  11986  sumeq2  12103  zsumdc  12129  fsum3  12132  fsumf1o  12135  fsum3cvg2  12139  fsumadd  12151  isummulc2  12171  fsum2d  12180  fsummulc2  12193  fsumconst  12199  modfsummod  12203  fsumparts  12215  fsumrelem  12216  fsumiun  12222  binom  12229  bcxmas  12234  isumshft  12235  isumnn0nn  12238  mertenslem2  12281  clim2prod  12284  prodfrecap  12291  prodeq2  12302  zproddc  12324  fprodseq  12328  fprodf1o  12333  prodsnf  12337  fprodfac  12360  fprodabs  12361  fprodconst  12365  fprod2d  12368  fprodrec  12374  fprodmodd  12386  efne0  12423  efexp  12427  demoivreALT  12519  moddvds  12544  bitsinv1  12707  gcddiv  12774  alginv  12803  algfx  12808  lcmneg  12830  lcmid  12836  lcmgcdeq  12839  divgcdcoprm0  12857  cncongr1  12859  cncongr2  12860  nn0gcdsq  12956  crth  12980  eulerthlema  12986  eulerthlemh  12987  pythagtriplem1  13022  pcqmul  13060  pcexp  13066  pcneg  13082  pcmpt  13100  pcfac  13107  1arith  13124  setscomd  13371  ercpbllemg  13628  mgmidmo  13669  mgmlrid  13676  lidrideqd  13678  lidrididd  13679  grpinvalem  13682  grpinva  13683  issgrp  13695  isnsgrp  13698  sgrpass  13700  sgrp1  13703  issgrpd  13704  sgrppropd  13705  ismndd  13727  mndpropd  13730  imasmnd2  13736  mnd1  13739  mnd1id  13740  ismhm  13745  mhmpropd  13750  mhmlin  13751  mhmeql  13776  isgrp  13788  grppropd  13799  isgrpd2e  13802  dfgrp2  13809  isgrpid2  13822  grpidd2  13823  grpinvfvalg  13824  grpinvpropdg  13857  grpidssd  13858  grpinvssd  13859  grpsubrcan  13863  dfgrp3mlem  13880  grplactcnv  13884  imasgrp2  13890  mhmlem  13894  mulgnn0p1  13913  mulgaddcom  13926  mulginvcom  13927  mulgneg2  13936  mulgnnass  13937  mulgnn0ass  13938  mulgass  13939  mhmmulg  13943  isghm  14023  ghmlin  14028  ghmeql  14047  iscmn  14073  cmnpropd  14075  iscmnd  14078  cmnsubm  14089  abladdsub4  14095  imasabl  14117  gzsumconst  14120  gsummptfidmadd  14138  gsumconstcmn  14143  isrng  14208  rngass  14213  rngdi  14214  rngdir  14215  rngpropd  14229  imasrng  14230  issrg  14243  srgmulgass  14267  srgpcomp  14268  srg1expzeq1  14273  isring  14278  iscrng2  14293  ringpropd  14316  ringinvnz1ne0  14327  mulgass2  14336  ring1  14337  imasring  14342  opprnegg  14362  dvdsrd  14374  dvreq1  14422  rhmmul  14444  isrhm2d  14445  rhmopp  14456  rhmunitinv  14458  islring  14472  opprlring  14477  rrgval  14543  unitrrg  14549  opprdomnbg  14556  islmod  14600  lmodlema  14601  islmodd  14602  lmodvsmmulgdi  14632  lmodprop2d  14657  rmodislmodlem  14659  rmodislmod  14660  rnglidlmsgrp  14806  rnglidlrng  14807  quscrng  14842  cnfldmulg  14885  cnfldexp  14886  gsumfsum  14895  zndvds  14956  znf1o  14958  znunit  14966  psr1clfi  15002  txcnp  15295  cnmpt11  15307  cnmpt21  15315  cnmptcom  15322  isxms  15475  xmspropd  15501  bdmopn  15528  dvexp  15735  dvmptfsum  15749  rpcxpmul2  15938  wilthlem1  16008  mpodvdsmulf1o  16018  fsumdvdsmul  16019  perfect  16029  lgsne0  16071  gausslemma2d  16102  lgseisenlem2  16104  lgsquad2lem2  16115  2lgslem1a  16121  2lgslem1b  16122  usgredg2v  16379  issubgr  16412  wkslem1  16475  wkslem2  16476  iswlk  16478  uspgr2wlkeq  16520  2wlklem  16531  wlkres  16534  eupth2lem3fi  16631  eupth2fi  16634  depindlem1  16661  depindlem2  16662  depindlem3  16663  depind  16664  nninffeq  16968