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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  cdeqeq  3046  sbceqg  3163  csbing  3438  uniprg  3950  unisng  3952  intprg  4003  iununir  4096  csbopabg  4210  undifexmid  4332  exmidundif  4345  exmidundifim  4346  limeq  4524  onsucuni2  4713  ordpwsucexmid  4719  csbima12g  5151  dmsnsnsng  5268  cnvsng  5276  csbiotag  5373  fvmptf  5801  eqfnfv2f  5813  fvreseq  5815  fmptco  5877  fnressn  5904  fvsng  5914  cocan1  5996  cocan2  5997  fliftfun  6005  csbriotag  6055  oveqrspc2v  6115  csbov123g  6127  eqfnov  6198  ovmpos  6215  ov2gf  6216  ovmpodxf  6217  caovcomg  6248  caovassg  6251  caovcang  6254  caovcanrd  6256  caovcan  6257  caovdig  6267  caovdirg  6270  caovimo  6286  offveqb  6326  caofid0l  6333  caofid0r  6334  op1stg  6388  op2ndg  6389  f1o2ndf1  6468  tfrlem1  6584  tfrlem3ag  6585  tfrlem3a  6586  tfrlem5  6590  tfrlem9  6595  tfr0dm  6598  tfrlemiubacc  6606  tfrlemiex  6607  tfrlemi1  6608  tfr1onlem3ag  6613  tfr1onlemubacc  6622  tfr1onlemex  6623  tfr1onlemaccex  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemubacc  6635  tfrcllemex  6636  tfrcllemaccex  6637  tfrcllemres  6638  tfrcldm  6639  tfri3  6643  rdg0g  6664  frecrdg  6684  nna0r  6756  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  ecopovtrn  6911  ecopovsymg  6913  ecopovtrng  6914  ecovcom  6921  ecovicom  6922  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  dom2lem  7064  ordiso2  7381  inl11  7411  updjud  7428  omp1eomlem  7440  difinfsnlem  7445  nnnninfeq  7474  nninfwlporlemd  7518  nninfwlpor  7520  nninfinfwlpo  7526  exmidfodomrlemrALT  7561  exmidaclem  7570  addcanpig  7707  mulcanpig  7708  mulcmpblnq  7741  mulpipqqs  7746  ordpipqqs  7747  mulidnq  7762  enq0sym  7805  nqnq0  7814  mulcmpblnq0  7817  distrnq0  7832  mulcomnq0  7833  addassnq0  7835  nq02m  7838  genipv  7882  cauappcvgprlemladd  8031  addcmpblnr  8112  0idsr  8140  1idsr  8141  axaddcom  8243  ax1rid  8250  ax0id  8251  rereceu  8262  axcaucvg  8273  mulrid  8329  readdcan  8473  cnegexlem1  8508  cnegexlem3  8510  addcan  8513  addcan2  8514  apti  8958  mulcanapd  8997  mulcanap2d  8998  div11ap  9038  divmuleqap  9055  conjmulap  9067  eqneg  9070  ofsubeq0  9300  cnref1o  10067  fzsuc2  10502  fzprval  10505  fztpval  10506  qtri3or  10691  modqadd1  10818  modqmul1  10834  addmodlteq  10855  frec2uzrdg  10866  frecuzrdgg  10873  seq3val  10917  seqvalcd  10918  seq3fveq2  10932  seqfveq2g  10934  seqfveqg  10935  seq3fveq  10936  seq3feq  10937  seq3shft2  10938  seqshft2g  10939  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seq3caopr2  10950  seqcaopr2g  10951  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemqk  10964  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1olemp  10972  seq3f1oleml  10973  seqf1oglem2a  10975  seqf1oglem2  10977  seqf1og  10978  seq3id  10982  seq3id2  10983  seq3homo  10984  seqhomog  10987  seqfeq4g  10988  mulexp  11035  expadd  11038  expmul  11041  modqexp  11124  nn0opth2d  11182  bcpasc  11225  bcm1n  11228  hashennn  11240  hashen  11244  omgadd  11263  hashfzo  11284  hashfzp1  11286  hashxp  11288  hashmap  11289  hashfibclem  11303  hashfibc  11304  hashfacen  11305  hashf1lem1  11306  hashf1lem2  11307  hashf1  11308  seq3coll  11315  eqs1  11417  swrdspsleq  11460  pfxeq  11489  pfxsuff1eqwrdeq  11492  ccatopth2  11510  cats1un  11514  swrdccatin1  11518  swrdccat3blem  11532  shftvalg  11622  shftval4g  11623  replim  11645  cjreb  11652  cjexp  11679  absexp  11867  recan  11897  minclpr  12026  mingeb  12032  sumeq2  12149  zsumdc  12175  fsum3  12178  fsumf1o  12181  fsum3cvg2  12185  fsumadd  12197  isummulc2  12217  fsum2d  12226  fsummulc2  12239  fsumconst  12245  modfsummod  12249  fsumparts  12261  fsumrelem  12262  fsumiun  12268  binom  12275  bcxmas  12280  isumshft  12281  isumnn0nn  12284  mertenslem2  12327  clim2prod  12330  prodfrecap  12337  prodeq2  12348  zproddc  12370  fprodseq  12374  fprodf1o  12379  prodsnf  12383  fprodfac  12406  fprodabs  12407  fprodconst  12411  fprod2d  12414  fprodrec  12420  fprodmodd  12432  efne0  12469  efexp  12473  demoivreALT  12565  moddvds  12590  bitsinv1  12753  gcddiv  12820  alginv  12849  algfx  12854  lcmneg  12876  lcmid  12882  lcmgcdeq  12885  divgcdcoprm0  12903  cncongr1  12905  cncongr2  12906  nn0gcdsq  13004  crth  13030  eulerthlema  13036  eulerthlemh  13037  pythagtriplem1  13072  pcqmul  13110  pcexp  13116  pcneg  13132  pcmpt  13150  pcfac  13157  1arith  13174  setscomd  13450  ercpbllemg  13709  mgmidmo  13750  mgmlrid  13757  lidrideqd  13759  lidrididd  13760  grpinvalem  13763  grpinva  13764  issgrp  13776  isnsgrp  13779  sgrpass  13781  sgrp1  13784  issgrpd  13785  sgrppropd  13786  ismndd  13808  mndpropd  13811  imasmnd2  13817  mnd1  13820  mnd1id  13821  ismhm  13826  mhmpropd  13831  mhmlin  13832  mhmeql  13857  isgrp  13869  grppropd  13880  isgrpd2e  13883  dfgrp2  13890  isgrpid2  13903  grpidd2  13904  grpinvfvalg  13905  grpinvpropdg  13938  grpidssd  13939  grpinvssd  13940  grpsubrcan  13944  dfgrp3mlem  13961  grplactcnv  13965  imasgrp2  13971  mhmlem  13975  mulgnn0p1  13994  mulgaddcom  14007  mulginvcom  14008  mulgneg2  14017  mulgnnass  14018  mulgnn0ass  14019  mulgass  14020  mhmmulg  14024  isghm  14104  ghmlin  14109  ghmeql  14128  cntzex  14149  cntzfval  14151  elcntz  14153  cntzsnval  14155  elcntzsn  14156  cntzi  14161  resscntz  14165  cntzmhm  14172  iscmn  14185  cmnpropd  14187  iscmnd  14190  cmnsubm  14201  abladdsub4  14207  imasabl  14229  gzsumconst  14232  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsumresfi  14262  gsumconstcmn  14265  gsum2dfilem2  14271  isrng  14339  rngass  14344  rngdi  14345  rngdir  14346  rngpropd  14360  imasrng  14361  issrg  14375  srgmulgass  14399  srgpcomp  14400  srg1expzeq1  14405  isring  14410  iscrng2  14425  ringpropd  14449  ringinvnz1ne0  14460  mulgass2  14469  ring1  14470  imasring  14477  opprnegg  14497  dvdsrd  14509  dvreq1  14557  rhmmul  14579  isrhm2d  14580  rhmopp  14591  rhmunitinv  14593  islring  14607  opprlring  14612  rrgval  14678  unitrrg  14684  opprdomnbg  14691  islmod  14735  lmodlema  14736  islmodd  14737  lmodvsmmulgdi  14768  lmodprop2d  14793  rmodislmodlem  14795  rmodislmod  14796  rnglidlmsgrp  14942  rnglidlrng  14943  quscrng  14978  cnfldmulg  15021  cnfldexp  15022  gsumfsum  15031  zndvds  15092  znf1o  15094  znunit  15102  isassa  15110  assalem  15111  isassad  15119  assapropd  15122  assamulgscm  15151  psr1clfi  15207  mvrf1fi  15219  txcnp  15514  cnmpt11  15526  cnmpt21  15534  cnmptcom  15541  isxms  15694  xmspropd  15720  bdmopn  15747  dvexp  15954  dvmptfsum  15968  sineq0re  16093  rpcxpmul2  16163  wilthlem1  16249  mpodvdsmulf1o  16301  fsumdvdsmul  16302  perfect  16318  lgsne0  16379  gausslemma2d  16410  lgseisenlem2  16412  lgsquad2lem2  16423  2lgslem1a  16429  2lgslem1b  16430  usgredg2v  16687  issubgr  16720  wkslem1  16783  wkslem2  16784  iswlk  16786  uspgr2wlkeq  16828  2wlklem  16839  wlkres  16842  eupth2lem3fi  16939  eupth2fi  16942  depindlem1  16969  depindlem2  16970  depindlem3  16971  depind  16972  nninffeq  17286