Theorem eqeq12d 2222

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 2220	. 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 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  cdeqeq  3000  sbceqg  3117  csbing  3388  uniprg  3879  unisng  3881  intprg  3932  iununir  4025  csbopabg  4138  undifexmid  4253  exmidundif  4266  exmidundifim  4267  limeq  4442  onsucuni2  4630  ordpwsucexmid  4636  csbima12g  5062  dmsnsnsng  5179  cnvsng  5187  csbiotag  5283  fvmptf  5695  eqfnfv2f  5704  fvreseq  5706  fmptco  5769  fnressn  5793  fvsng  5803  cocan1  5879  cocan2  5880  fliftfun  5888  csbriotag  5935  oveqrspc2v  5994  csbov123g  6006  eqfnov  6075  ovmpos  6092  ov2gf  6093  ovmpodxf  6094  caovcomg  6125  caovassg  6128  caovcang  6131  caovcanrd  6133  caovcan  6134  caovdig  6144  caovdirg  6147  caovimo  6163  offveqb  6201  caofid0l  6208  caofid0r  6209  op1stg  6259  op2ndg  6260  f1o2ndf1  6337  tfrlem1  6417  tfrlem3ag  6418  tfrlem3a  6419  tfrlem5  6423  tfrlem9  6428  tfr0dm  6431  tfrlemiubacc  6439  tfrlemiex  6440  tfrlemi1  6441  tfr1onlem3ag  6446  tfr1onlemubacc  6455  tfr1onlemex  6456  tfr1onlemaccex  6457  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemubacc  6468  tfrcllemex  6469  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  tfri3  6476  rdg0g  6497  frecrdg  6517  nna0r  6587  nnacom  6593  nnaass  6594  nndi  6595  nnmass  6596  nnmsucr  6597  nnmcom  6598  ecopovtrn  6742  ecopovsymg  6744  ecopovtrng  6745  ecovcom  6752  ecovicom  6753  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  dom2lem  6886  ordiso2  7163  inl11  7193  updjud  7210  omp1eomlem  7222  difinfsnlem  7227  nnnninfeq  7256  nninfwlporlemd  7300  nninfwlpor  7302  nninfinfwlpo  7308  exmidfodomrlemrALT  7342  exmidaclem  7351  addcanpig  7482  mulcanpig  7483  mulcmpblnq  7516  mulpipqqs  7521  ordpipqqs  7522  mulidnq  7537  enq0sym  7580  nqnq0  7589  mulcmpblnq0  7592  distrnq0  7607  mulcomnq0  7608  addassnq0  7610  nq02m  7613  genipv  7657  cauappcvgprlemladd  7806  addcmpblnr  7887  0idsr  7915  1idsr  7916  axaddcom  8018  ax1rid  8025  ax0id  8026  rereceu  8037  axcaucvg  8048  mulrid  8104  readdcan  8247  cnegexlem1  8282  cnegexlem3  8284  addcan  8287  addcan2  8288  apti  8730  mulcanapd  8769  mulcanap2d  8770  div11ap  8808  divmuleqap  8825  conjmulap  8837  eqneg  8840  cnref1o  9807  fzsuc2  10236  fzprval  10239  fztpval  10240  qtri3or  10420  modqadd1  10543  modqmul1  10559  addmodlteq  10580  frec2uzrdg  10591  frecuzrdgg  10598  seq3val  10642  seqvalcd  10643  seq3fveq2  10657  seqfveq2g  10659  seqfveqg  10660  seq3fveq  10661  seq3feq  10662  seq3shft2  10663  seqshft2g  10664  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seq3caopr2  10675  seqcaopr2g  10676  iseqf1olemkle  10679  iseqf1olemklt  10680  iseqf1olemqk  10689  seq3f1olemqsum  10695  seq3f1olemstep  10696  seq3f1olemp  10697  seq3f1oleml  10698  seqf1oglem2a  10700  seqf1oglem2  10702  seqf1og  10703  seq3id  10707  seq3id2  10708  seq3homo  10709  seqhomog  10712  seqfeq4g  10713  mulexp  10760  expadd  10763  expmul  10766  modqexp  10848  nn0opth2d  10905  bcpasc  10948  hashennn  10962  hashen  10966  omgadd  10984  hashfzo  11004  hashfzp1  11006  hashxp  11008  hashfacen  11018  seq3coll  11024  eqs1  11120  swrdspsleq  11158  pfxeq  11187  pfxsuff1eqwrdeq  11190  ccatopth2  11208  cats1un  11212  swrdccatin1  11216  swrdccat3blem  11230  shftvalg  11262  shftval4g  11263  replim  11285  cjreb  11292  cjexp  11319  absexp  11505  recan  11535  minclpr  11663  mingeb  11668  sumeq2  11785  zsumdc  11810  fsum3  11813  fsumf1o  11816  fsum3cvg2  11820  fsumadd  11832  isummulc2  11852  fsum2d  11861  fsummulc2  11874  fsumconst  11880  modfsummod  11884  fsumparts  11896  fsumrelem  11897  fsumiun  11903  binom  11910  bcxmas  11915  isumshft  11916  isumnn0nn  11919  mertenslem2  11962  clim2prod  11965  prodfrecap  11972  prodeq2  11983  zproddc  12005  fprodseq  12009  fprodf1o  12014  prodsnf  12018  fprodfac  12041  fprodabs  12042  fprodconst  12046  fprod2d  12049  fprodrec  12055  fprodmodd  12067  efne0  12104  efexp  12108  demoivreALT  12200  moddvds  12225  bitsinv1  12388  gcddiv  12455  alginv  12484  algfx  12489  lcmneg  12511  lcmid  12517  lcmgcdeq  12520  divgcdcoprm0  12538  cncongr1  12540  cncongr2  12541  nn0gcdsq  12637  crth  12661  eulerthlema  12667  eulerthlemh  12668  pythagtriplem1  12703  pcqmul  12741  pcexp  12747  pcneg  12763  pcmpt  12781  pcfac  12788  1arith  12805  setscomd  12988  ercpbllemg  13277  mgmidmo  13319  mgmlrid  13326  lidrideqd  13328  lidrididd  13329  grpinvalem  13332  grpinva  13333  issgrp  13350  isnsgrp  13353  sgrpass  13355  sgrp1  13358  issgrpd  13359  sgrppropd  13360  ismndd  13384  mndpropd  13387  imasmnd2  13399  mnd1  13402  mnd1id  13403  ismhm  13408  mhmpropd  13413  mhmlin  13414  mhmeql  13439  isgrp  13453  grppropd  13464  isgrpd2e  13467  dfgrp2  13474  isgrpid2  13487  grpidd2  13488  grpinvfvalg  13489  grpinvpropdg  13522  grpidssd  13523  grpinvssd  13524  grpsubrcan  13528  dfgrp3mlem  13545  grplactcnv  13549  imasgrp2  13561  mhmlem  13565  mulgnn0p1  13584  mulgaddcom  13597  mulginvcom  13598  mulgneg2  13607  mulgnnass  13608  mulgnn0ass  13609  mulgass  13610  mhmmulg  13614  isghm  13694  ghmlin  13699  ghmeql  13718  iscmn  13744  cmnpropd  13746  iscmnd  13749  abladdsub4  13765  imasabl  13787  gsumfzconst  13792  isrng  13811  rngass  13816  rngdi  13817  rngdir  13818  rngpropd  13832  imasrng  13833  issrg  13842  srgmulgass  13866  srgpcomp  13867  srg1expzeq1  13872  isring  13877  iscrng2  13892  ringpropd  13915  ringinvnz1ne0  13926  mulgass2  13935  ring1  13936  imasring  13941  opprnegg  13960  dvdsrd  13971  dvreq1  14019  rhmmul  14041  isrhm2d  14042  rhmopp  14053  rhmunitinv  14055  islring  14069  rrgval  14139  unitrrg  14144  opprdomnbg  14151  islmod  14168  lmodlema  14169  islmodd  14170  lmodvsmmulgdi  14200  lmodprop2d  14225  rmodislmodlem  14227  rmodislmod  14228  rnglidlmsgrp  14374  rnglidlrng  14375  quscrng  14410  cnfldmulg  14453  cnfldexp  14454  gsumfzfsumlemm  14464  zndvds  14526  znf1o  14528  znunit  14536  psr1clfi  14565  txcnp  14858  cnmpt11  14870  cnmpt21  14878  cnmptcom  14885  isxms  15038  xmspropd  15064  bdmopn  15091  dvexp  15298  dvmptfsum  15312  rpcxpmul2  15500  wilthlem1  15567  mpodvdsmulf1o  15577  fsumdvdsmul  15578  perfect  15588  lgsne0  15630  gausslemma2d  15661  lgseisenlem2  15663  lgsquad2lem2  15674  2lgslem1a  15680  2lgslem1b  15681  nninffeq  16159