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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  cdeqeq  3027  sbceqg  3144  csbing  3416  uniprg  3913  unisng  3915  intprg  3966  iununir  4059  csbopabg  4172  undifexmid  4289  exmidundif  4302  exmidundifim  4303  limeq  4480  onsucuni2  4668  ordpwsucexmid  4674  csbima12g  5104  dmsnsnsng  5221  cnvsng  5229  csbiotag  5326  fvmptf  5748  eqfnfv2f  5757  fvreseq  5759  fmptco  5821  fnressn  5848  fvsng  5858  cocan1  5938  cocan2  5939  fliftfun  5947  csbriotag  5995  oveqrspc2v  6055  csbov123g  6067  eqfnov  6138  ovmpos  6155  ov2gf  6156  ovmpodxf  6157  caovcomg  6188  caovassg  6191  caovcang  6194  caovcanrd  6196  caovcan  6197  caovdig  6207  caovdirg  6210  caovimo  6226  offveqb  6264  caofid0l  6271  caofid0r  6272  op1stg  6322  op2ndg  6323  f1o2ndf1  6402  tfrlem1  6517  tfrlem3ag  6518  tfrlem3a  6519  tfrlem5  6523  tfrlem9  6528  tfr0dm  6531  tfrlemiubacc  6539  tfrlemiex  6540  tfrlemi1  6541  tfr1onlem3ag  6546  tfr1onlemubacc  6555  tfr1onlemex  6556  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemubacc  6568  tfrcllemex  6569  tfrcllemaccex  6570  tfrcllemres  6571  tfrcldm  6572  tfri3  6576  rdg0g  6597  frecrdg  6617  nna0r  6689  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  ecopovtrn  6844  ecopovsymg  6846  ecopovtrng  6847  ecovcom  6854  ecovicom  6855  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  dom2lem  6988  ordiso2  7277  inl11  7307  updjud  7324  omp1eomlem  7336  difinfsnlem  7341  nnnninfeq  7370  nninfwlporlemd  7414  nninfwlpor  7416  nninfinfwlpo  7422  exmidfodomrlemrALT  7457  exmidaclem  7466  addcanpig  7597  mulcanpig  7598  mulcmpblnq  7631  mulpipqqs  7636  ordpipqqs  7637  mulidnq  7652  enq0sym  7695  nqnq0  7704  mulcmpblnq0  7707  distrnq0  7722  mulcomnq0  7723  addassnq0  7725  nq02m  7728  genipv  7772  cauappcvgprlemladd  7921  addcmpblnr  8002  0idsr  8030  1idsr  8031  axaddcom  8133  ax1rid  8140  ax0id  8141  rereceu  8152  axcaucvg  8163  mulrid  8219  readdcan  8361  cnegexlem1  8396  cnegexlem3  8398  addcan  8401  addcan2  8402  apti  8844  mulcanapd  8883  mulcanap2d  8884  div11ap  8922  divmuleqap  8939  conjmulap  8951  eqneg  8954  cnref1o  9929  fzsuc2  10359  fzprval  10362  fztpval  10363  qtri3or  10546  modqadd1  10669  modqmul1  10685  addmodlteq  10706  frec2uzrdg  10717  frecuzrdgg  10724  seq3val  10768  seqvalcd  10769  seq3fveq2  10783  seqfveq2g  10785  seqfveqg  10786  seq3fveq  10787  seq3feq  10788  seq3shft2  10789  seqshft2g  10790  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  seq3caopr2  10801  seqcaopr2g  10802  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqk  10815  seq3f1olemqsum  10821  seq3f1olemstep  10822  seq3f1olemp  10823  seq3f1oleml  10824  seqf1oglem2a  10826  seqf1oglem2  10828  seqf1og  10829  seq3id  10833  seq3id2  10834  seq3homo  10835  seqhomog  10838  seqfeq4g  10839  mulexp  10886  expadd  10889  expmul  10892  modqexp  10974  nn0opth2d  11031  bcpasc  11074  hashennn  11088  hashen  11092  omgadd  11111  hashfzo  11132  hashfzp1  11134  hashxp  11136  hashfacen  11146  seq3coll  11152  eqs1  11254  swrdspsleq  11297  pfxeq  11326  pfxsuff1eqwrdeq  11329  ccatopth2  11347  cats1un  11351  swrdccatin1  11355  swrdccat3blem  11369  shftvalg  11459  shftval4g  11460  replim  11482  cjreb  11489  cjexp  11516  absexp  11702  recan  11732  minclpr  11860  mingeb  11865  sumeq2  11982  zsumdc  12008  fsum3  12011  fsumf1o  12014  fsum3cvg2  12018  fsumadd  12030  isummulc2  12050  fsum2d  12059  fsummulc2  12072  fsumconst  12078  modfsummod  12082  fsumparts  12094  fsumrelem  12095  fsumiun  12101  binom  12108  bcxmas  12113  isumshft  12114  isumnn0nn  12117  mertenslem2  12160  clim2prod  12163  prodfrecap  12170  prodeq2  12181  zproddc  12203  fprodseq  12207  fprodf1o  12212  prodsnf  12216  fprodfac  12239  fprodabs  12240  fprodconst  12244  fprod2d  12247  fprodrec  12253  fprodmodd  12265  efne0  12302  efexp  12306  demoivreALT  12398  moddvds  12423  bitsinv1  12586  gcddiv  12653  alginv  12682  algfx  12687  lcmneg  12709  lcmid  12715  lcmgcdeq  12718  divgcdcoprm0  12736  cncongr1  12738  cncongr2  12739  nn0gcdsq  12835  crth  12859  eulerthlema  12865  eulerthlemh  12866  pythagtriplem1  12901  pcqmul  12939  pcexp  12945  pcneg  12961  pcmpt  12979  pcfac  12986  1arith  13003  setscomd  13186  ercpbllemg  13476  mgmidmo  13518  mgmlrid  13525  lidrideqd  13527  lidrididd  13528  grpinvalem  13531  grpinva  13532  issgrp  13549  isnsgrp  13552  sgrpass  13554  sgrp1  13557  issgrpd  13558  sgrppropd  13559  ismndd  13583  mndpropd  13586  imasmnd2  13598  mnd1  13601  mnd1id  13602  ismhm  13607  mhmpropd  13612  mhmlin  13613  mhmeql  13638  isgrp  13652  grppropd  13663  isgrpd2e  13666  dfgrp2  13673  isgrpid2  13686  grpidd2  13687  grpinvfvalg  13688  grpinvpropdg  13721  grpidssd  13722  grpinvssd  13723  grpsubrcan  13727  dfgrp3mlem  13744  grplactcnv  13748  imasgrp2  13760  mhmlem  13764  mulgnn0p1  13783  mulgaddcom  13796  mulginvcom  13797  mulgneg2  13806  mulgnnass  13807  mulgnn0ass  13808  mulgass  13809  mhmmulg  13813  isghm  13893  ghmlin  13898  ghmeql  13917  iscmn  13943  cmnpropd  13945  iscmnd  13948  abladdsub4  13964  imasabl  13986  gsumfzconst  13991  isrng  14011  rngass  14016  rngdi  14017  rngdir  14018  rngpropd  14032  imasrng  14033  issrg  14042  srgmulgass  14066  srgpcomp  14067  srg1expzeq1  14072  isring  14077  iscrng2  14092  ringpropd  14115  ringinvnz1ne0  14126  mulgass2  14135  ring1  14136  imasring  14141  opprnegg  14160  dvdsrd  14172  dvreq1  14220  rhmmul  14242  isrhm2d  14243  rhmopp  14254  rhmunitinv  14256  islring  14270  rrgval  14340  unitrrg  14346  opprdomnbg  14353  islmod  14370  lmodlema  14371  islmodd  14372  lmodvsmmulgdi  14402  lmodprop2d  14427  rmodislmodlem  14429  rmodislmod  14430  rnglidlmsgrp  14576  rnglidlrng  14577  quscrng  14612  cnfldmulg  14655  cnfldexp  14656  gsumfzfsumlemm  14666  zndvds  14728  znf1o  14730  znunit  14738  psr1clfi  14772  txcnp  15065  cnmpt11  15077  cnmpt21  15085  cnmptcom  15092  isxms  15245  xmspropd  15271  bdmopn  15298  dvexp  15505  dvmptfsum  15519  rpcxpmul2  15707  wilthlem1  15777  mpodvdsmulf1o  15787  fsumdvdsmul  15788  perfect  15798  lgsne0  15840  gausslemma2d  15871  lgseisenlem2  15873  lgsquad2lem2  15884  2lgslem1a  15890  2lgslem1b  15891  usgredg2v  16148  issubgr  16181  wkslem1  16244  wkslem2  16245  iswlk  16247  uspgr2wlkeq  16289  2wlklem  16300  wlkres  16303  eupth2lem3fi  16400  eupth2fi  16403  depindlem1  16430  depindlem2  16431  depindlem3  16432  depind  16433  nninffeq  16729