Theorem eqeq12d 2246

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 2244	. 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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  cdeqeq  3026  sbceqg  3143  csbing  3414  uniprg  3908  unisng  3910  intprg  3961  iununir  4054  csbopabg  4167  undifexmid  4283  exmidundif  4296  exmidundifim  4297  limeq  4474  onsucuni2  4662  ordpwsucexmid  4668  csbima12g  5097  dmsnsnsng  5214  cnvsng  5222  csbiotag  5319  fvmptf  5739  eqfnfv2f  5748  fvreseq  5750  fmptco  5813  fnressn  5839  fvsng  5849  cocan1  5927  cocan2  5928  fliftfun  5936  csbriotag  5984  oveqrspc2v  6044  csbov123g  6056  eqfnov  6127  ovmpos  6144  ov2gf  6145  ovmpodxf  6146  caovcomg  6177  caovassg  6180  caovcang  6183  caovcanrd  6185  caovcan  6186  caovdig  6196  caovdirg  6199  caovimo  6215  offveqb  6254  caofid0l  6261  caofid0r  6262  op1stg  6312  op2ndg  6313  f1o2ndf1  6392  tfrlem1  6473  tfrlem3ag  6474  tfrlem3a  6475  tfrlem5  6479  tfrlem9  6484  tfr0dm  6487  tfrlemiubacc  6495  tfrlemiex  6496  tfrlemi1  6497  tfr1onlem3ag  6502  tfr1onlemubacc  6511  tfr1onlemex  6512  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemubacc  6524  tfrcllemex  6525  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  tfri3  6532  rdg0g  6553  frecrdg  6573  nna0r  6645  nnacom  6651  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  ecopovtrn  6800  ecopovsymg  6802  ecopovtrng  6803  ecovcom  6810  ecovicom  6811  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  dom2lem  6944  ordiso2  7233  inl11  7263  updjud  7280  omp1eomlem  7292  difinfsnlem  7297  nnnninfeq  7326  nninfwlporlemd  7370  nninfwlpor  7372  nninfinfwlpo  7378  exmidfodomrlemrALT  7413  exmidaclem  7422  addcanpig  7553  mulcanpig  7554  mulcmpblnq  7587  mulpipqqs  7592  ordpipqqs  7593  mulidnq  7608  enq0sym  7651  nqnq0  7660  mulcmpblnq0  7663  distrnq0  7678  mulcomnq0  7679  addassnq0  7681  nq02m  7684  genipv  7728  cauappcvgprlemladd  7877  addcmpblnr  7958  0idsr  7986  1idsr  7987  axaddcom  8089  ax1rid  8096  ax0id  8097  rereceu  8108  axcaucvg  8119  mulrid  8175  readdcan  8318  cnegexlem1  8353  cnegexlem3  8355  addcan  8358  addcan2  8359  apti  8801  mulcanapd  8840  mulcanap2d  8841  div11ap  8879  divmuleqap  8896  conjmulap  8908  eqneg  8911  cnref1o  9884  fzsuc2  10313  fzprval  10316  fztpval  10317  qtri3or  10499  modqadd1  10622  modqmul1  10638  addmodlteq  10659  frec2uzrdg  10670  frecuzrdgg  10677  seq3val  10721  seqvalcd  10722  seq3fveq2  10736  seqfveq2g  10738  seqfveqg  10739  seq3fveq  10740  seq3feq  10741  seq3shft2  10742  seqshft2g  10743  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seq3caopr2  10754  seqcaopr2g  10755  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqk  10768  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1olemp  10776  seq3f1oleml  10777  seqf1oglem2a  10779  seqf1oglem2  10781  seqf1og  10782  seq3id  10786  seq3id2  10787  seq3homo  10788  seqhomog  10791  seqfeq4g  10792  mulexp  10839  expadd  10842  expmul  10845  modqexp  10927  nn0opth2d  10984  bcpasc  11027  hashennn  11041  hashen  11045  omgadd  11064  hashfzo  11085  hashfzp1  11087  hashxp  11089  hashfacen  11099  seq3coll  11105  eqs1  11204  swrdspsleq  11247  pfxeq  11276  pfxsuff1eqwrdeq  11279  ccatopth2  11297  cats1un  11301  swrdccatin1  11305  swrdccat3blem  11319  shftvalg  11396  shftval4g  11397  replim  11419  cjreb  11426  cjexp  11453  absexp  11639  recan  11669  minclpr  11797  mingeb  11802  sumeq2  11919  zsumdc  11944  fsum3  11947  fsumf1o  11950  fsum3cvg2  11954  fsumadd  11966  isummulc2  11986  fsum2d  11995  fsummulc2  12008  fsumconst  12014  modfsummod  12018  fsumparts  12030  fsumrelem  12031  fsumiun  12037  binom  12044  bcxmas  12049  isumshft  12050  isumnn0nn  12053  mertenslem2  12096  clim2prod  12099  prodfrecap  12106  prodeq2  12117  zproddc  12139  fprodseq  12143  fprodf1o  12148  prodsnf  12152  fprodfac  12175  fprodabs  12176  fprodconst  12180  fprod2d  12183  fprodrec  12189  fprodmodd  12201  efne0  12238  efexp  12242  demoivreALT  12334  moddvds  12359  bitsinv1  12522  gcddiv  12589  alginv  12618  algfx  12623  lcmneg  12645  lcmid  12651  lcmgcdeq  12654  divgcdcoprm0  12672  cncongr1  12674  cncongr2  12675  nn0gcdsq  12771  crth  12795  eulerthlema  12801  eulerthlemh  12802  pythagtriplem1  12837  pcqmul  12875  pcexp  12881  pcneg  12897  pcmpt  12915  pcfac  12922  1arith  12939  setscomd  13122  ercpbllemg  13412  mgmidmo  13454  mgmlrid  13461  lidrideqd  13463  lidrididd  13464  grpinvalem  13467  grpinva  13468  issgrp  13485  isnsgrp  13488  sgrpass  13490  sgrp1  13493  issgrpd  13494  sgrppropd  13495  ismndd  13519  mndpropd  13522  imasmnd2  13534  mnd1  13537  mnd1id  13538  ismhm  13543  mhmpropd  13548  mhmlin  13549  mhmeql  13574  isgrp  13588  grppropd  13599  isgrpd2e  13602  dfgrp2  13609  isgrpid2  13622  grpidd2  13623  grpinvfvalg  13624  grpinvpropdg  13657  grpidssd  13658  grpinvssd  13659  grpsubrcan  13663  dfgrp3mlem  13680  grplactcnv  13684  imasgrp2  13696  mhmlem  13700  mulgnn0p1  13719  mulgaddcom  13732  mulginvcom  13733  mulgneg2  13742  mulgnnass  13743  mulgnn0ass  13744  mulgass  13745  mhmmulg  13749  isghm  13829  ghmlin  13834  ghmeql  13853  iscmn  13879  cmnpropd  13881  iscmnd  13884  abladdsub4  13900  imasabl  13922  gsumfzconst  13927  isrng  13946  rngass  13951  rngdi  13952  rngdir  13953  rngpropd  13967  imasrng  13968  issrg  13977  srgmulgass  14001  srgpcomp  14002  srg1expzeq1  14007  isring  14012  iscrng2  14027  ringpropd  14050  ringinvnz1ne0  14061  mulgass2  14070  ring1  14071  imasring  14076  opprnegg  14095  dvdsrd  14107  dvreq1  14155  rhmmul  14177  isrhm2d  14178  rhmopp  14189  rhmunitinv  14191  islring  14205  rrgval  14275  unitrrg  14280  opprdomnbg  14287  islmod  14304  lmodlema  14305  islmodd  14306  lmodvsmmulgdi  14336  lmodprop2d  14361  rmodislmodlem  14363  rmodislmod  14364  rnglidlmsgrp  14510  rnglidlrng  14511  quscrng  14546  cnfldmulg  14589  cnfldexp  14590  gsumfzfsumlemm  14600  zndvds  14662  znf1o  14664  znunit  14672  psr1clfi  14701  txcnp  14994  cnmpt11  15006  cnmpt21  15014  cnmptcom  15021  isxms  15174  xmspropd  15200  bdmopn  15227  dvexp  15434  dvmptfsum  15448  rpcxpmul2  15636  wilthlem1  15703  mpodvdsmulf1o  15713  fsumdvdsmul  15714  perfect  15724  lgsne0  15766  gausslemma2d  15797  lgseisenlem2  15799  lgsquad2lem2  15810  2lgslem1a  15816  2lgslem1b  15817  usgredg2v  16074  issubgr  16107  wkslem1  16170  wkslem2  16171  iswlk  16173  uspgr2wlkeq  16215  2wlklem  16226  wlkres  16229  nninffeq  16622