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  8467  cnegexlem1  8502  cnegexlem3  8504  addcan  8507  addcan2  8508  apti  8952  mulcanapd  8991  mulcanap2d  8992  div11ap  9032  divmuleqap  9049  conjmulap  9061  eqneg  9064  cnref1o  10061  fzsuc2  10496  fzprval  10499  fztpval  10500  qtri3or  10685  modqadd1  10811  modqmul1  10827  addmodlteq  10848  frec2uzrdg  10859  frecuzrdgg  10866  seq3val  10910  seqvalcd  10911  seq3fveq2  10925  seqfveq2g  10927  seqfveqg  10928  seq3fveq  10929  seq3feq  10930  seq3shft2  10931  seqshft2g  10932  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seq3caopr2  10943  seqcaopr2g  10944  iseqf1olemkle  10947  iseqf1olemklt  10948  iseqf1olemqk  10957  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1olemp  10965  seq3f1oleml  10966  seqf1oglem2a  10968  seqf1oglem2  10970  seqf1og  10971  seq3id  10975  seq3id2  10976  seq3homo  10977  seqhomog  10980  seqfeq4g  10981  mulexp  11028  expadd  11031  expmul  11034  modqexp  11117  nn0opth2d  11175  bcpasc  11218  bcm1n  11221  hashennn  11233  hashen  11237  omgadd  11256  hashfzo  11277  hashfzp1  11279  hashxp  11281  hashmap  11282  hashfibclem  11296  hashfibc  11297  hashfacen  11298  hashf1lem1  11299  hashf1lem2  11300  hashf1  11301  seq3coll  11308  eqs1  11410  swrdspsleq  11453  pfxeq  11482  pfxsuff1eqwrdeq  11485  ccatopth2  11503  cats1un  11507  swrdccatin1  11511  swrdccat3blem  11525  shftvalg  11615  shftval4g  11616  replim  11638  cjreb  11645  cjexp  11672  absexp  11860  recan  11890  minclpr  12018  mingeb  12024  sumeq2  12141  zsumdc  12167  fsum3  12170  fsumf1o  12173  fsum3cvg2  12177  fsumadd  12189  isummulc2  12209  fsum2d  12218  fsummulc2  12231  fsumconst  12237  modfsummod  12241  fsumparts  12253  fsumrelem  12254  fsumiun  12260  binom  12267  bcxmas  12272  isumshft  12273  isumnn0nn  12276  mertenslem2  12319  clim2prod  12322  prodfrecap  12329  prodeq2  12340  zproddc  12362  fprodseq  12366  fprodf1o  12371  prodsnf  12375  fprodfac  12398  fprodabs  12399  fprodconst  12403  fprod2d  12406  fprodrec  12412  fprodmodd  12424  efne0  12461  efexp  12465  demoivreALT  12557  moddvds  12582  bitsinv1  12745  gcddiv  12812  alginv  12841  algfx  12846  lcmneg  12868  lcmid  12874  lcmgcdeq  12877  divgcdcoprm0  12895  cncongr1  12897  cncongr2  12898  nn0gcdsq  12996  crth  13022  eulerthlema  13028  eulerthlemh  13029  pythagtriplem1  13064  pcqmul  13102  pcexp  13108  pcneg  13124  pcmpt  13142  pcfac  13149  1arith  13166  setscomd  13442  ercpbllemg  13700  mgmidmo  13741  mgmlrid  13748  lidrideqd  13750  lidrididd  13751  grpinvalem  13754  grpinva  13755  issgrp  13767  isnsgrp  13770  sgrpass  13772  sgrp1  13775  issgrpd  13776  sgrppropd  13777  ismndd  13799  mndpropd  13802  imasmnd2  13808  mnd1  13811  mnd1id  13812  ismhm  13817  mhmpropd  13822  mhmlin  13823  mhmeql  13848  isgrp  13860  grppropd  13871  isgrpd2e  13874  dfgrp2  13881  isgrpid2  13894  grpidd2  13895  grpinvfvalg  13896  grpinvpropdg  13929  grpidssd  13930  grpinvssd  13931  grpsubrcan  13935  dfgrp3mlem  13952  grplactcnv  13956  imasgrp2  13962  mhmlem  13966  mulgnn0p1  13985  mulgaddcom  13998  mulginvcom  13999  mulgneg2  14008  mulgnnass  14009  mulgnn0ass  14010  mulgass  14011  mhmmulg  14015  isghm  14095  ghmlin  14100  ghmeql  14119  iscmn  14145  cmnpropd  14147  iscmnd  14150  cmnsubm  14161  abladdsub4  14167  imasabl  14189  gzsumconst  14192  gsummptfidmadd  14210  gsumconstcmn  14215  isrng  14282  rngass  14287  rngdi  14288  rngdir  14289  rngpropd  14303  imasrng  14304  issrg  14318  srgmulgass  14342  srgpcomp  14343  srg1expzeq1  14348  isring  14353  iscrng2  14368  ringpropd  14392  ringinvnz1ne0  14403  mulgass2  14412  ring1  14413  imasring  14418  opprnegg  14438  dvdsrd  14450  dvreq1  14498  rhmmul  14520  isrhm2d  14521  rhmopp  14532  rhmunitinv  14534  islring  14548  opprlring  14553  rrgval  14619  unitrrg  14625  opprdomnbg  14632  islmod  14676  lmodlema  14677  islmodd  14678  lmodvsmmulgdi  14709  lmodprop2d  14734  rmodislmodlem  14736  rmodislmod  14737  rnglidlmsgrp  14883  rnglidlrng  14884  quscrng  14919  cnfldmulg  14962  cnfldexp  14963  gsumfsum  14972  zndvds  15033  znf1o  15035  znunit  15043  isassa  15051  assalem  15052  isassad  15060  assapropd  15063  assamulgscm  15092  psr1clfi  15128  txcnp  15421  cnmpt11  15433  cnmpt21  15441  cnmptcom  15448  isxms  15601  xmspropd  15627  bdmopn  15654  dvexp  15861  dvmptfsum  15875  rpcxpmul2  16068  wilthlem1  16151  mpodvdsmulf1o  16185  fsumdvdsmul  16186  perfect  16199  lgsne0  16255  gausslemma2d  16286  lgseisenlem2  16288  lgsquad2lem2  16299  2lgslem1a  16305  2lgslem1b  16306  usgredg2v  16563  issubgr  16596  wkslem1  16659  wkslem2  16660  iswlk  16662  uspgr2wlkeq  16704  2wlklem  16715  wlkres  16718  eupth2lem3fi  16815  eupth2fi  16818  depindlem1  16845  depindlem2  16846  depindlem3  16847  depind  16848  nninffeq  17161