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  4209  undifexmid  4330  exmidundif  4343  exmidundifim  4344  limeq  4522  onsucuni2  4711  ordpwsucexmid  4717  csbima12g  5148  dmsnsnsng  5265  cnvsng  5273  csbiotag  5370  fvmptf  5798  eqfnfv2f  5810  fvreseq  5812  fmptco  5874  fnressn  5901  fvsng  5911  cocan1  5993  cocan2  5994  fliftfun  6002  csbriotag  6052  oveqrspc2v  6112  csbov123g  6124  eqfnov  6195  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  caovcomg  6245  caovassg  6248  caovcang  6251  caovcanrd  6253  caovcan  6254  caovdig  6264  caovdirg  6267  caovimo  6283  offveqb  6322  caofid0l  6329  caofid0r  6330  op1stg  6384  op2ndg  6385  f1o2ndf1  6464  tfrlem1  6579  tfrlem3ag  6580  tfrlem3a  6581  tfrlem5  6585  tfrlem9  6590  tfr0dm  6593  tfrlemiubacc  6601  tfrlemiex  6602  tfrlemi1  6603  tfr1onlem3ag  6608  tfr1onlemubacc  6617  tfr1onlemex  6618  tfr1onlemaccex  6619  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemubacc  6630  tfrcllemex  6631  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  tfri3  6638  rdg0g  6659  frecrdg  6679  nna0r  6751  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  dom2lem  7058  ordiso2  7375  inl11  7405  updjud  7422  omp1eomlem  7434  difinfsnlem  7439  nnnninfeq  7468  nninfwlporlemd  7512  nninfwlpor  7514  nninfinfwlpo  7520  exmidfodomrlemrALT  7555  exmidaclem  7564  addcanpig  7701  mulcanpig  7702  mulcmpblnq  7735  mulpipqqs  7740  ordpipqqs  7741  mulidnq  7756  enq0sym  7799  nqnq0  7808  mulcmpblnq0  7811  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  nq02m  7832  genipv  7876  cauappcvgprlemladd  8025  addcmpblnr  8106  0idsr  8134  1idsr  8135  axaddcom  8237  ax1rid  8244  ax0id  8245  rereceu  8256  axcaucvg  8267  mulrid  8323  readdcan  8466  cnegexlem1  8501  cnegexlem3  8503  addcan  8506  addcan2  8507  apti  8950  mulcanapd  8989  mulcanap2d  8990  div11ap  9030  divmuleqap  9047  conjmulap  9059  eqneg  9062  cnref1o  10051  fzsuc2  10486  fzprval  10489  fztpval  10490  qtri3or  10675  modqadd1  10798  modqmul1  10814  addmodlteq  10835  frec2uzrdg  10846  frecuzrdgg  10853  seq3val  10897  seqvalcd  10898  seq3fveq2  10912  seqfveq2g  10914  seqfveqg  10915  seq3fveq  10916  seq3feq  10917  seq3shft2  10918  seqshft2g  10919  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemkle  10934  iseqf1olemklt  10935  iseqf1olemqk  10944  seq3f1olemqsum  10950  seq3f1olemstep  10951  seq3f1olemp  10952  seq3f1oleml  10953  seqf1oglem2a  10955  seqf1oglem2  10957  seqf1og  10958  seq3id  10962  seq3id2  10963  seq3homo  10964  seqhomog  10967  seqfeq4g  10968  mulexp  11015  expadd  11018  expmul  11021  modqexp  11104  nn0opth2d  11161  bcpasc  11204  bcm1n  11207  hashennn  11219  hashen  11223  omgadd  11242  hashfzo  11263  hashfzp1  11265  hashxp  11267  hashmap  11268  hashfibclem  11282  hashfibc  11283  hashfacen  11284  hashf1lem1  11285  hashf1lem2  11286  hashf1  11287  seq3coll  11294  eqs1  11396  swrdspsleq  11439  pfxeq  11468  pfxsuff1eqwrdeq  11471  ccatopth2  11489  cats1un  11493  swrdccatin1  11497  swrdccat3blem  11511  shftvalg  11601  shftval4g  11602  replim  11624  cjreb  11631  cjexp  11658  absexp  11845  recan  11875  minclpr  12003  mingeb  12008  sumeq2  12125  zsumdc  12151  fsum3  12154  fsumf1o  12157  fsum3cvg2  12161  fsumadd  12173  isummulc2  12193  fsum2d  12202  fsummulc2  12215  fsumconst  12221  modfsummod  12225  fsumparts  12237  fsumrelem  12238  fsumiun  12244  binom  12251  bcxmas  12256  isumshft  12257  isumnn0nn  12260  mertenslem2  12303  clim2prod  12306  prodfrecap  12313  prodeq2  12324  zproddc  12346  fprodseq  12350  fprodf1o  12355  prodsnf  12359  fprodfac  12382  fprodabs  12383  fprodconst  12387  fprod2d  12390  fprodrec  12396  fprodmodd  12408  efne0  12445  efexp  12449  demoivreALT  12541  moddvds  12566  bitsinv1  12729  gcddiv  12796  alginv  12825  algfx  12830  lcmneg  12852  lcmid  12858  lcmgcdeq  12861  divgcdcoprm0  12879  cncongr1  12881  cncongr2  12882  nn0gcdsq  12978  crth  13002  eulerthlema  13008  eulerthlemh  13009  pythagtriplem1  13044  pcqmul  13082  pcexp  13088  pcneg  13104  pcmpt  13122  pcfac  13129  1arith  13146  setscomd  13393  ercpbllemg  13651  mgmidmo  13692  mgmlrid  13699  lidrideqd  13701  lidrididd  13702  grpinvalem  13705  grpinva  13706  issgrp  13718  isnsgrp  13721  sgrpass  13723  sgrp1  13726  issgrpd  13727  sgrppropd  13728  ismndd  13750  mndpropd  13753  imasmnd2  13759  mnd1  13762  mnd1id  13763  ismhm  13768  mhmpropd  13773  mhmlin  13774  mhmeql  13799  isgrp  13811  grppropd  13822  isgrpd2e  13825  dfgrp2  13832  isgrpid2  13845  grpidd2  13846  grpinvfvalg  13847  grpinvpropdg  13880  grpidssd  13881  grpinvssd  13882  grpsubrcan  13886  dfgrp3mlem  13903  grplactcnv  13907  imasgrp2  13913  mhmlem  13917  mulgnn0p1  13936  mulgaddcom  13949  mulginvcom  13950  mulgneg2  13959  mulgnnass  13960  mulgnn0ass  13961  mulgass  13962  mhmmulg  13966  isghm  14046  ghmlin  14051  ghmeql  14070  iscmn  14096  cmnpropd  14098  iscmnd  14101  cmnsubm  14112  abladdsub4  14118  imasabl  14140  gzsumconst  14143  gsummptfidmadd  14161  gsumconstcmn  14166  isrng  14233  rngass  14238  rngdi  14239  rngdir  14240  rngpropd  14254  imasrng  14255  issrg  14269  srgmulgass  14293  srgpcomp  14294  srg1expzeq1  14299  isring  14304  iscrng2  14319  ringpropd  14343  ringinvnz1ne0  14354  mulgass2  14363  ring1  14364  imasring  14369  opprnegg  14389  dvdsrd  14401  dvreq1  14449  rhmmul  14471  isrhm2d  14472  rhmopp  14483  rhmunitinv  14485  islring  14499  opprlring  14504  rrgval  14570  unitrrg  14576  opprdomnbg  14583  islmod  14627  lmodlema  14628  islmodd  14629  lmodvsmmulgdi  14660  lmodprop2d  14685  rmodislmodlem  14687  rmodislmod  14688  rnglidlmsgrp  14834  rnglidlrng  14835  quscrng  14870  cnfldmulg  14913  cnfldexp  14914  gsumfsum  14923  zndvds  14984  znf1o  14986  znunit  14994  isassa  15002  assalem  15003  isassad  15011  assapropd  15014  assamulgscm  15043  psr1clfi  15079  txcnp  15372  cnmpt11  15384  cnmpt21  15392  cnmptcom  15399  isxms  15552  xmspropd  15578  bdmopn  15605  dvexp  15812  dvmptfsum  15826  rpcxpmul2  16015  wilthlem1  16094  mpodvdsmulf1o  16104  fsumdvdsmul  16105  perfect  16115  lgsne0  16157  gausslemma2d  16188  lgseisenlem2  16190  lgsquad2lem2  16201  2lgslem1a  16207  2lgslem1b  16208  usgredg2v  16465  issubgr  16498  wkslem1  16561  wkslem2  16562  iswlk  16564  uspgr2wlkeq  16606  2wlklem  16617  wlkres  16620  eupth2lem3fi  16717  eupth2fi  16720  depindlem1  16747  depindlem2  16748  depindlem3  16749  depind  16750  nninffeq  17063