Theorem eqeq12d 2244

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 2242	. 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 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  cdeqeq  3024  sbceqg  3141  csbing  3412  uniprg  3906  unisng  3908  intprg  3959  iununir  4052  csbopabg  4165  undifexmid  4281  exmidundif  4294  exmidundifim  4295  limeq  4472  onsucuni2  4660  ordpwsucexmid  4666  csbima12g  5095  dmsnsnsng  5212  cnvsng  5220  csbiotag  5317  fvmptf  5735  eqfnfv2f  5744  fvreseq  5746  fmptco  5809  fnressn  5835  fvsng  5845  cocan1  5923  cocan2  5924  fliftfun  5932  csbriotag  5980  oveqrspc2v  6040  csbov123g  6052  eqfnov  6123  ovmpos  6140  ov2gf  6141  ovmpodxf  6142  caovcomg  6173  caovassg  6176  caovcang  6179  caovcanrd  6181  caovcan  6182  caovdig  6192  caovdirg  6195  caovimo  6211  offveqb  6250  caofid0l  6257  caofid0r  6258  op1stg  6308  op2ndg  6309  f1o2ndf1  6388  tfrlem1  6469  tfrlem3ag  6470  tfrlem3a  6471  tfrlem5  6475  tfrlem9  6480  tfr0dm  6483  tfrlemiubacc  6491  tfrlemiex  6492  tfrlemi1  6493  tfr1onlem3ag  6498  tfr1onlemubacc  6507  tfr1onlemex  6508  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemubacc  6520  tfrcllemex  6521  tfrcllemaccex  6522  tfrcllemres  6523  tfrcldm  6524  tfri3  6528  rdg0g  6549  frecrdg  6569  nna0r  6641  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  ecopovtrn  6796  ecopovsymg  6798  ecopovtrng  6799  ecovcom  6806  ecovicom  6807  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  dom2lem  6940  ordiso2  7225  inl11  7255  updjud  7272  omp1eomlem  7284  difinfsnlem  7289  nnnninfeq  7318  nninfwlporlemd  7362  nninfwlpor  7364  nninfinfwlpo  7370  exmidfodomrlemrALT  7404  exmidaclem  7413  addcanpig  7544  mulcanpig  7545  mulcmpblnq  7578  mulpipqqs  7583  ordpipqqs  7584  mulidnq  7599  enq0sym  7642  nqnq0  7651  mulcmpblnq0  7654  distrnq0  7669  mulcomnq0  7670  addassnq0  7672  nq02m  7675  genipv  7719  cauappcvgprlemladd  7868  addcmpblnr  7949  0idsr  7977  1idsr  7978  axaddcom  8080  ax1rid  8087  ax0id  8088  rereceu  8099  axcaucvg  8110  mulrid  8166  readdcan  8309  cnegexlem1  8344  cnegexlem3  8346  addcan  8349  addcan2  8350  apti  8792  mulcanapd  8831  mulcanap2d  8832  div11ap  8870  divmuleqap  8887  conjmulap  8899  eqneg  8902  cnref1o  9875  fzsuc2  10304  fzprval  10307  fztpval  10308  qtri3or  10490  modqadd1  10613  modqmul1  10629  addmodlteq  10650  frec2uzrdg  10661  frecuzrdgg  10668  seq3val  10712  seqvalcd  10713  seq3fveq2  10727  seqfveq2g  10729  seqfveqg  10730  seq3fveq  10731  seq3feq  10732  seq3shft2  10733  seqshft2g  10734  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seq3caopr2  10745  seqcaopr2g  10746  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemqk  10759  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1olemp  10767  seq3f1oleml  10768  seqf1oglem2a  10770  seqf1oglem2  10772  seqf1og  10773  seq3id  10777  seq3id2  10778  seq3homo  10779  seqhomog  10782  seqfeq4g  10783  mulexp  10830  expadd  10833  expmul  10836  modqexp  10918  nn0opth2d  10975  bcpasc  11018  hashennn  11032  hashen  11036  omgadd  11055  hashfzo  11076  hashfzp1  11078  hashxp  11080  hashfacen  11090  seq3coll  11096  eqs1  11195  swrdspsleq  11238  pfxeq  11267  pfxsuff1eqwrdeq  11270  ccatopth2  11288  cats1un  11292  swrdccatin1  11296  swrdccat3blem  11310  shftvalg  11387  shftval4g  11388  replim  11410  cjreb  11417  cjexp  11444  absexp  11630  recan  11660  minclpr  11788  mingeb  11793  sumeq2  11910  zsumdc  11935  fsum3  11938  fsumf1o  11941  fsum3cvg2  11945  fsumadd  11957  isummulc2  11977  fsum2d  11986  fsummulc2  11999  fsumconst  12005  modfsummod  12009  fsumparts  12021  fsumrelem  12022  fsumiun  12028  binom  12035  bcxmas  12040  isumshft  12041  isumnn0nn  12044  mertenslem2  12087  clim2prod  12090  prodfrecap  12097  prodeq2  12108  zproddc  12130  fprodseq  12134  fprodf1o  12139  prodsnf  12143  fprodfac  12166  fprodabs  12167  fprodconst  12171  fprod2d  12174  fprodrec  12180  fprodmodd  12192  efne0  12229  efexp  12233  demoivreALT  12325  moddvds  12350  bitsinv1  12513  gcddiv  12580  alginv  12609  algfx  12614  lcmneg  12636  lcmid  12642  lcmgcdeq  12645  divgcdcoprm0  12663  cncongr1  12665  cncongr2  12666  nn0gcdsq  12762  crth  12786  eulerthlema  12792  eulerthlemh  12793  pythagtriplem1  12828  pcqmul  12866  pcexp  12872  pcneg  12888  pcmpt  12906  pcfac  12913  1arith  12930  setscomd  13113  ercpbllemg  13403  mgmidmo  13445  mgmlrid  13452  lidrideqd  13454  lidrididd  13455  grpinvalem  13458  grpinva  13459  issgrp  13476  isnsgrp  13479  sgrpass  13481  sgrp1  13484  issgrpd  13485  sgrppropd  13486  ismndd  13510  mndpropd  13513  imasmnd2  13525  mnd1  13528  mnd1id  13529  ismhm  13534  mhmpropd  13539  mhmlin  13540  mhmeql  13565  isgrp  13579  grppropd  13590  isgrpd2e  13593  dfgrp2  13600  isgrpid2  13613  grpidd2  13614  grpinvfvalg  13615  grpinvpropdg  13648  grpidssd  13649  grpinvssd  13650  grpsubrcan  13654  dfgrp3mlem  13671  grplactcnv  13675  imasgrp2  13687  mhmlem  13691  mulgnn0p1  13710  mulgaddcom  13723  mulginvcom  13724  mulgneg2  13733  mulgnnass  13734  mulgnn0ass  13735  mulgass  13736  mhmmulg  13740  isghm  13820  ghmlin  13825  ghmeql  13844  iscmn  13870  cmnpropd  13872  iscmnd  13875  abladdsub4  13891  imasabl  13913  gsumfzconst  13918  isrng  13937  rngass  13942  rngdi  13943  rngdir  13944  rngpropd  13958  imasrng  13959  issrg  13968  srgmulgass  13992  srgpcomp  13993  srg1expzeq1  13998  isring  14003  iscrng2  14018  ringpropd  14041  ringinvnz1ne0  14052  mulgass2  14061  ring1  14062  imasring  14067  opprnegg  14086  dvdsrd  14098  dvreq1  14146  rhmmul  14168  isrhm2d  14169  rhmopp  14180  rhmunitinv  14182  islring  14196  rrgval  14266  unitrrg  14271  opprdomnbg  14278  islmod  14295  lmodlema  14296  islmodd  14297  lmodvsmmulgdi  14327  lmodprop2d  14352  rmodislmodlem  14354  rmodislmod  14355  rnglidlmsgrp  14501  rnglidlrng  14502  quscrng  14537  cnfldmulg  14580  cnfldexp  14581  gsumfzfsumlemm  14591  zndvds  14653  znf1o  14655  znunit  14663  psr1clfi  14692  txcnp  14985  cnmpt11  14997  cnmpt21  15005  cnmptcom  15012  isxms  15165  xmspropd  15191  bdmopn  15218  dvexp  15425  dvmptfsum  15439  rpcxpmul2  15627  wilthlem1  15694  mpodvdsmulf1o  15704  fsumdvdsmul  15705  perfect  15715  lgsne0  15757  gausslemma2d  15788  lgseisenlem2  15790  lgsquad2lem2  15801  2lgslem1a  15807  2lgslem1b  15808  usgredg2v  16063  wkslem1  16117  wkslem2  16118  iswlk  16120  uspgr2wlkeq  16162  2wlklem  16171  wlkres  16174  nninffeq  16558