Theorem eqeq12d 2219

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 2217	. 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 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  cdeqeq  2992  sbceqg  3108  csbing  3379  uniprg  3864  unisng  3866  intprg  3917  iununir  4010  csbopabg  4121  undifexmid  4236  exmidundif  4249  exmidundifim  4250  limeq  4423  onsucuni2  4611  ordpwsucexmid  4617  csbima12g  5042  dmsnsnsng  5159  cnvsng  5167  csbiotag  5263  fvmptf  5671  eqfnfv2f  5680  fvreseq  5682  fmptco  5745  fnressn  5769  fvsng  5779  cocan1  5855  cocan2  5856  fliftfun  5864  csbriotag  5911  oveqrspc2v  5970  csbov123g  5982  eqfnov  6051  ovmpos  6068  ov2gf  6069  ovmpodxf  6070  caovcomg  6101  caovassg  6104  caovcang  6107  caovcanrd  6109  caovcan  6110  caovdig  6120  caovdirg  6123  caovimo  6139  offveqb  6177  caofid0l  6184  caofid0r  6185  op1stg  6235  op2ndg  6236  f1o2ndf1  6313  tfrlem1  6393  tfrlem3ag  6394  tfrlem3a  6395  tfrlem5  6399  tfrlem9  6404  tfr0dm  6407  tfrlemiubacc  6415  tfrlemiex  6416  tfrlemi1  6417  tfr1onlem3ag  6422  tfr1onlemubacc  6431  tfr1onlemex  6432  tfr1onlemaccex  6433  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllemubacc  6444  tfrcllemex  6445  tfrcllemaccex  6446  tfrcllemres  6447  tfrcldm  6448  tfri3  6452  rdg0g  6473  frecrdg  6493  nna0r  6563  nnacom  6569  nnaass  6570  nndi  6571  nnmass  6572  nnmsucr  6573  nnmcom  6574  ecopovtrn  6718  ecopovsymg  6720  ecopovtrng  6721  ecovcom  6728  ecovicom  6729  ecovass  6730  ecoviass  6731  ecovdi  6732  ecovidi  6733  dom2lem  6862  ordiso2  7136  inl11  7166  updjud  7183  omp1eomlem  7195  difinfsnlem  7200  nnnninfeq  7229  nninfwlporlemd  7273  nninfwlpor  7275  nninfinfwlpo  7281  exmidfodomrlemrALT  7310  exmidaclem  7319  addcanpig  7446  mulcanpig  7447  mulcmpblnq  7480  mulpipqqs  7485  ordpipqqs  7486  mulidnq  7501  enq0sym  7544  nqnq0  7553  mulcmpblnq0  7556  distrnq0  7571  mulcomnq0  7572  addassnq0  7574  nq02m  7577  genipv  7621  cauappcvgprlemladd  7770  addcmpblnr  7851  0idsr  7879  1idsr  7880  axaddcom  7982  ax1rid  7989  ax0id  7990  rereceu  8001  axcaucvg  8012  mulrid  8068  readdcan  8211  cnegexlem1  8246  cnegexlem3  8248  addcan  8251  addcan2  8252  apti  8694  mulcanapd  8733  mulcanap2d  8734  div11ap  8772  divmuleqap  8789  conjmulap  8801  eqneg  8804  cnref1o  9771  fzsuc2  10200  fzprval  10203  fztpval  10204  qtri3or  10381  modqadd1  10504  modqmul1  10520  addmodlteq  10541  frec2uzrdg  10552  frecuzrdgg  10559  seq3val  10603  seqvalcd  10604  seq3fveq2  10618  seqfveq2g  10620  seqfveqg  10621  seq3fveq  10622  seq3feq  10623  seq3shft2  10624  seqshft2g  10625  seq3split  10631  seqsplitg  10632  seq3caopr3  10634  seqcaopr3g  10635  seq3caopr2  10636  seqcaopr2g  10637  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqk  10650  seq3f1olemqsum  10656  seq3f1olemstep  10657  seq3f1olemp  10658  seq3f1oleml  10659  seqf1oglem2a  10661  seqf1oglem2  10663  seqf1og  10664  seq3id  10668  seq3id2  10669  seq3homo  10670  seqhomog  10673  seqfeq4g  10674  mulexp  10721  expadd  10724  expmul  10727  modqexp  10809  nn0opth2d  10866  bcpasc  10909  hashennn  10923  hashen  10927  omgadd  10945  hashfzo  10965  hashfzp1  10967  hashxp  10969  hashfacen  10979  seq3coll  10985  eqs1  11080  shftvalg  11118  shftval4g  11119  replim  11141  cjreb  11148  cjexp  11175  absexp  11361  recan  11391  minclpr  11519  mingeb  11524  sumeq2  11641  zsumdc  11666  fsum3  11669  fsumf1o  11672  fsum3cvg2  11676  fsumadd  11688  isummulc2  11708  fsum2d  11717  fsummulc2  11730  fsumconst  11736  modfsummod  11740  fsumparts  11752  fsumrelem  11753  fsumiun  11759  binom  11766  bcxmas  11771  isumshft  11772  isumnn0nn  11775  mertenslem2  11818  clim2prod  11821  prodfrecap  11828  prodeq2  11839  zproddc  11861  fprodseq  11865  fprodf1o  11870  prodsnf  11874  fprodfac  11897  fprodabs  11898  fprodconst  11902  fprod2d  11905  fprodrec  11911  fprodmodd  11923  efne0  11960  efexp  11964  demoivreALT  12056  moddvds  12081  bitsinv1  12244  gcddiv  12311  alginv  12340  algfx  12345  lcmneg  12367  lcmid  12373  lcmgcdeq  12376  divgcdcoprm0  12394  cncongr1  12396  cncongr2  12397  nn0gcdsq  12493  crth  12517  eulerthlema  12523  eulerthlemh  12524  pythagtriplem1  12559  pcqmul  12597  pcexp  12603  pcneg  12619  pcmpt  12637  pcfac  12644  1arith  12661  setscomd  12844  ercpbllemg  13133  mgmidmo  13175  mgmlrid  13182  lidrideqd  13184  lidrididd  13185  grpinvalem  13188  grpinva  13189  issgrp  13206  isnsgrp  13209  sgrpass  13211  sgrp1  13214  issgrpd  13215  sgrppropd  13216  ismndd  13240  mndpropd  13243  imasmnd2  13255  mnd1  13258  mnd1id  13259  ismhm  13264  mhmpropd  13269  mhmlin  13270  mhmeql  13295  isgrp  13309  grppropd  13320  isgrpd2e  13323  dfgrp2  13330  isgrpid2  13343  grpidd2  13344  grpinvfvalg  13345  grpinvpropdg  13378  grpidssd  13379  grpinvssd  13380  grpsubrcan  13384  dfgrp3mlem  13401  grplactcnv  13405  imasgrp2  13417  mhmlem  13421  mulgnn0p1  13440  mulgaddcom  13453  mulginvcom  13454  mulgneg2  13463  mulgnnass  13464  mulgnn0ass  13465  mulgass  13466  mhmmulg  13470  isghm  13550  ghmlin  13555  ghmeql  13574  iscmn  13600  cmnpropd  13602  iscmnd  13605  abladdsub4  13621  imasabl  13643  gsumfzconst  13648  isrng  13667  rngass  13672  rngdi  13673  rngdir  13674  rngpropd  13688  imasrng  13689  issrg  13698  srgmulgass  13722  srgpcomp  13723  srg1expzeq1  13728  isring  13733  iscrng2  13748  ringpropd  13771  ringinvnz1ne0  13782  mulgass2  13791  ring1  13792  imasring  13797  opprnegg  13816  dvdsrd  13827  dvreq1  13875  rhmmul  13897  isrhm2d  13898  rhmopp  13909  rhmunitinv  13911  islring  13925  rrgval  13995  unitrrg  14000  opprdomnbg  14007  islmod  14024  lmodlema  14025  islmodd  14026  lmodvsmmulgdi  14056  lmodprop2d  14081  rmodislmodlem  14083  rmodislmod  14084  rnglidlmsgrp  14230  rnglidlrng  14231  quscrng  14266  cnfldmulg  14309  cnfldexp  14310  gsumfzfsumlemm  14320  zndvds  14382  znf1o  14384  znunit  14392  psr1clfi  14421  txcnp  14714  cnmpt11  14726  cnmpt21  14734  cnmptcom  14741  isxms  14894  xmspropd  14920  bdmopn  14947  dvexp  15154  dvmptfsum  15168  rpcxpmul2  15356  wilthlem1  15423  mpodvdsmulf1o  15433  fsumdvdsmul  15434  perfect  15444  lgsne0  15486  gausslemma2d  15517  lgseisenlem2  15519  lgsquad2lem2  15530  2lgslem1a  15536  2lgslem1b  15537  nninffeq  15919