Theorem eqeq12d 2244

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 2242	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  cdeqeq  3023  sbceqg  3140  csbing  3411  uniprg  3903  unisng  3905  intprg  3956  iununir  4049  csbopabg  4162  undifexmid  4277  exmidundif  4290  exmidundifim  4291  limeq  4468  onsucuni2  4656  ordpwsucexmid  4662  csbima12g  5089  dmsnsnsng  5206  cnvsng  5214  csbiotag  5311  fvmptf  5729  eqfnfv2f  5738  fvreseq  5740  fmptco  5803  fnressn  5829  fvsng  5839  cocan1  5917  cocan2  5918  fliftfun  5926  csbriotag  5974  oveqrspc2v  6034  csbov123g  6046  eqfnov  6117  ovmpos  6134  ov2gf  6135  ovmpodxf  6136  caovcomg  6167  caovassg  6170  caovcang  6173  caovcanrd  6175  caovcan  6176  caovdig  6186  caovdirg  6189  caovimo  6205  offveqb  6244  caofid0l  6251  caofid0r  6252  op1stg  6302  op2ndg  6303  f1o2ndf1  6380  tfrlem1  6460  tfrlem3ag  6461  tfrlem3a  6462  tfrlem5  6466  tfrlem9  6471  tfr0dm  6474  tfrlemiubacc  6482  tfrlemiex  6483  tfrlemi1  6484  tfr1onlem3ag  6489  tfr1onlemubacc  6498  tfr1onlemex  6499  tfr1onlemaccex  6500  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemubacc  6511  tfrcllemex  6512  tfrcllemaccex  6513  tfrcllemres  6514  tfrcldm  6515  tfri3  6519  rdg0g  6540  frecrdg  6560  nna0r  6632  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  ecopovtrn  6787  ecopovsymg  6789  ecopovtrng  6790  ecovcom  6797  ecovicom  6798  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  dom2lem  6931  ordiso2  7213  inl11  7243  updjud  7260  omp1eomlem  7272  difinfsnlem  7277  nnnninfeq  7306  nninfwlporlemd  7350  nninfwlpor  7352  nninfinfwlpo  7358  exmidfodomrlemrALT  7392  exmidaclem  7401  addcanpig  7532  mulcanpig  7533  mulcmpblnq  7566  mulpipqqs  7571  ordpipqqs  7572  mulidnq  7587  enq0sym  7630  nqnq0  7639  mulcmpblnq0  7642  distrnq0  7657  mulcomnq0  7658  addassnq0  7660  nq02m  7663  genipv  7707  cauappcvgprlemladd  7856  addcmpblnr  7937  0idsr  7965  1idsr  7966  axaddcom  8068  ax1rid  8075  ax0id  8076  rereceu  8087  axcaucvg  8098  mulrid  8154  readdcan  8297  cnegexlem1  8332  cnegexlem3  8334  addcan  8337  addcan2  8338  apti  8780  mulcanapd  8819  mulcanap2d  8820  div11ap  8858  divmuleqap  8875  conjmulap  8887  eqneg  8890  cnref1o  9858  fzsuc2  10287  fzprval  10290  fztpval  10291  qtri3or  10472  modqadd1  10595  modqmul1  10611  addmodlteq  10632  frec2uzrdg  10643  frecuzrdgg  10650  seq3val  10694  seqvalcd  10695  seq3fveq2  10709  seqfveq2g  10711  seqfveqg  10712  seq3fveq  10713  seq3feq  10714  seq3shft2  10715  seqshft2g  10716  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqk  10741  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1olemp  10749  seq3f1oleml  10750  seqf1oglem2a  10752  seqf1oglem2  10754  seqf1og  10755  seq3id  10759  seq3id2  10760  seq3homo  10761  seqhomog  10764  seqfeq4g  10765  mulexp  10812  expadd  10815  expmul  10818  modqexp  10900  nn0opth2d  10957  bcpasc  11000  hashennn  11014  hashen  11018  omgadd  11036  hashfzo  11057  hashfzp1  11059  hashxp  11061  hashfacen  11071  seq3coll  11077  eqs1  11176  swrdspsleq  11214  pfxeq  11243  pfxsuff1eqwrdeq  11246  ccatopth2  11264  cats1un  11268  swrdccatin1  11272  swrdccat3blem  11286  shftvalg  11362  shftval4g  11363  replim  11385  cjreb  11392  cjexp  11419  absexp  11605  recan  11635  minclpr  11763  mingeb  11768  sumeq2  11885  zsumdc  11910  fsum3  11913  fsumf1o  11916  fsum3cvg2  11920  fsumadd  11932  isummulc2  11952  fsum2d  11961  fsummulc2  11974  fsumconst  11980  modfsummod  11984  fsumparts  11996  fsumrelem  11997  fsumiun  12003  binom  12010  bcxmas  12015  isumshft  12016  isumnn0nn  12019  mertenslem2  12062  clim2prod  12065  prodfrecap  12072  prodeq2  12083  zproddc  12105  fprodseq  12109  fprodf1o  12114  prodsnf  12118  fprodfac  12141  fprodabs  12142  fprodconst  12146  fprod2d  12149  fprodrec  12155  fprodmodd  12167  efne0  12204  efexp  12208  demoivreALT  12300  moddvds  12325  bitsinv1  12488  gcddiv  12555  alginv  12584  algfx  12589  lcmneg  12611  lcmid  12617  lcmgcdeq  12620  divgcdcoprm0  12638  cncongr1  12640  cncongr2  12641  nn0gcdsq  12737  crth  12761  eulerthlema  12767  eulerthlemh  12768  pythagtriplem1  12803  pcqmul  12841  pcexp  12847  pcneg  12863  pcmpt  12881  pcfac  12888  1arith  12905  setscomd  13088  ercpbllemg  13378  mgmidmo  13420  mgmlrid  13427  lidrideqd  13429  lidrididd  13430  grpinvalem  13433  grpinva  13434  issgrp  13451  isnsgrp  13454  sgrpass  13456  sgrp1  13459  issgrpd  13460  sgrppropd  13461  ismndd  13485  mndpropd  13488  imasmnd2  13500  mnd1  13503  mnd1id  13504  ismhm  13509  mhmpropd  13514  mhmlin  13515  mhmeql  13540  isgrp  13554  grppropd  13565  isgrpd2e  13568  dfgrp2  13575  isgrpid2  13588  grpidd2  13589  grpinvfvalg  13590  grpinvpropdg  13623  grpidssd  13624  grpinvssd  13625  grpsubrcan  13629  dfgrp3mlem  13646  grplactcnv  13650  imasgrp2  13662  mhmlem  13666  mulgnn0p1  13685  mulgaddcom  13698  mulginvcom  13699  mulgneg2  13708  mulgnnass  13709  mulgnn0ass  13710  mulgass  13711  mhmmulg  13715  isghm  13795  ghmlin  13800  ghmeql  13819  iscmn  13845  cmnpropd  13847  iscmnd  13850  abladdsub4  13866  imasabl  13888  gsumfzconst  13893  isrng  13912  rngass  13917  rngdi  13918  rngdir  13919  rngpropd  13933  imasrng  13934  issrg  13943  srgmulgass  13967  srgpcomp  13968  srg1expzeq1  13973  isring  13978  iscrng2  13993  ringpropd  14016  ringinvnz1ne0  14027  mulgass2  14036  ring1  14037  imasring  14042  opprnegg  14061  dvdsrd  14073  dvreq1  14121  rhmmul  14143  isrhm2d  14144  rhmopp  14155  rhmunitinv  14157  islring  14171  rrgval  14241  unitrrg  14246  opprdomnbg  14253  islmod  14270  lmodlema  14271  islmodd  14272  lmodvsmmulgdi  14302  lmodprop2d  14327  rmodislmodlem  14329  rmodislmod  14330  rnglidlmsgrp  14476  rnglidlrng  14477  quscrng  14512  cnfldmulg  14555  cnfldexp  14556  gsumfzfsumlemm  14566  zndvds  14628  znf1o  14630  znunit  14638  psr1clfi  14667  txcnp  14960  cnmpt11  14972  cnmpt21  14980  cnmptcom  14987  isxms  15140  xmspropd  15166  bdmopn  15193  dvexp  15400  dvmptfsum  15414  rpcxpmul2  15602  wilthlem1  15669  mpodvdsmulf1o  15679  fsumdvdsmul  15680  perfect  15690  lgsne0  15732  gausslemma2d  15763  lgseisenlem2  15765  lgsquad2lem2  15776  2lgslem1a  15782  2lgslem1b  15783  usgredg2v  16037  wkslem1  16061  wkslem2  16062  iswlk  16064  uspgr2wlkeq  16106  2wlklem  16115  wlkres  16118  nninffeq  16446