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  3023  sbceqg  3140  csbing  3411  uniprg  3902  unisng  3904  intprg  3955  iununir  4048  csbopabg  4161  undifexmid  4276  exmidundif  4289  exmidundifim  4290  limeq  4467  onsucuni2  4655  ordpwsucexmid  4661  csbima12g  5088  dmsnsnsng  5205  cnvsng  5213  csbiotag  5310  fvmptf  5726  eqfnfv2f  5735  fvreseq  5737  fmptco  5800  fnressn  5824  fvsng  5834  cocan1  5910  cocan2  5911  fliftfun  5919  csbriotag  5967  oveqrspc2v  6027  csbov123g  6039  eqfnov  6110  ovmpos  6127  ov2gf  6128  ovmpodxf  6129  caovcomg  6160  caovassg  6163  caovcang  6166  caovcanrd  6168  caovcan  6169  caovdig  6179  caovdirg  6182  caovimo  6198  offveqb  6236  caofid0l  6243  caofid0r  6244  op1stg  6294  op2ndg  6295  f1o2ndf1  6372  tfrlem1  6452  tfrlem3ag  6453  tfrlem3a  6454  tfrlem5  6458  tfrlem9  6463  tfr0dm  6466  tfrlemiubacc  6474  tfrlemiex  6475  tfrlemi1  6476  tfr1onlem3ag  6481  tfr1onlemubacc  6490  tfr1onlemex  6491  tfr1onlemaccex  6492  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllemubacc  6503  tfrcllemex  6504  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  tfri3  6511  rdg0g  6532  frecrdg  6552  nna0r  6622  nnacom  6628  nnaass  6629  nndi  6630  nnmass  6631  nnmsucr  6632  nnmcom  6633  ecopovtrn  6777  ecopovsymg  6779  ecopovtrng  6780  ecovcom  6787  ecovicom  6788  ecovass  6789  ecoviass  6790  ecovdi  6791  ecovidi  6792  dom2lem  6921  ordiso2  7198  inl11  7228  updjud  7245  omp1eomlem  7257  difinfsnlem  7262  nnnninfeq  7291  nninfwlporlemd  7335  nninfwlpor  7337  nninfinfwlpo  7343  exmidfodomrlemrALT  7377  exmidaclem  7386  addcanpig  7517  mulcanpig  7518  mulcmpblnq  7551  mulpipqqs  7556  ordpipqqs  7557  mulidnq  7572  enq0sym  7615  nqnq0  7624  mulcmpblnq0  7627  distrnq0  7642  mulcomnq0  7643  addassnq0  7645  nq02m  7648  genipv  7692  cauappcvgprlemladd  7841  addcmpblnr  7922  0idsr  7950  1idsr  7951  axaddcom  8053  ax1rid  8060  ax0id  8061  rereceu  8072  axcaucvg  8083  mulrid  8139  readdcan  8282  cnegexlem1  8317  cnegexlem3  8319  addcan  8322  addcan2  8323  apti  8765  mulcanapd  8804  mulcanap2d  8805  div11ap  8843  divmuleqap  8860  conjmulap  8872  eqneg  8875  cnref1o  9842  fzsuc2  10271  fzprval  10274  fztpval  10275  qtri3or  10455  modqadd1  10578  modqmul1  10594  addmodlteq  10615  frec2uzrdg  10626  frecuzrdgg  10633  seq3val  10677  seqvalcd  10678  seq3fveq2  10692  seqfveq2g  10694  seqfveqg  10695  seq3fveq  10696  seq3feq  10697  seq3shft2  10698  seqshft2g  10699  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  seq3caopr2  10710  seqcaopr2g  10711  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqk  10724  seq3f1olemqsum  10730  seq3f1olemstep  10731  seq3f1olemp  10732  seq3f1oleml  10733  seqf1oglem2a  10735  seqf1oglem2  10737  seqf1og  10738  seq3id  10742  seq3id2  10743  seq3homo  10744  seqhomog  10747  seqfeq4g  10748  mulexp  10795  expadd  10798  expmul  10801  modqexp  10883  nn0opth2d  10940  bcpasc  10983  hashennn  10997  hashen  11001  omgadd  11019  hashfzo  11039  hashfzp1  11041  hashxp  11043  hashfacen  11053  seq3coll  11059  eqs1  11156  swrdspsleq  11194  pfxeq  11223  pfxsuff1eqwrdeq  11226  ccatopth2  11244  cats1un  11248  swrdccatin1  11252  swrdccat3blem  11266  shftvalg  11342  shftval4g  11343  replim  11365  cjreb  11372  cjexp  11399  absexp  11585  recan  11615  minclpr  11743  mingeb  11748  sumeq2  11865  zsumdc  11890  fsum3  11893  fsumf1o  11896  fsum3cvg2  11900  fsumadd  11912  isummulc2  11932  fsum2d  11941  fsummulc2  11954  fsumconst  11960  modfsummod  11964  fsumparts  11976  fsumrelem  11977  fsumiun  11983  binom  11990  bcxmas  11995  isumshft  11996  isumnn0nn  11999  mertenslem2  12042  clim2prod  12045  prodfrecap  12052  prodeq2  12063  zproddc  12085  fprodseq  12089  fprodf1o  12094  prodsnf  12098  fprodfac  12121  fprodabs  12122  fprodconst  12126  fprod2d  12129  fprodrec  12135  fprodmodd  12147  efne0  12184  efexp  12188  demoivreALT  12280  moddvds  12305  bitsinv1  12468  gcddiv  12535  alginv  12564  algfx  12569  lcmneg  12591  lcmid  12597  lcmgcdeq  12600  divgcdcoprm0  12618  cncongr1  12620  cncongr2  12621  nn0gcdsq  12717  crth  12741  eulerthlema  12747  eulerthlemh  12748  pythagtriplem1  12783  pcqmul  12821  pcexp  12827  pcneg  12843  pcmpt  12861  pcfac  12868  1arith  12885  setscomd  13068  ercpbllemg  13358  mgmidmo  13400  mgmlrid  13407  lidrideqd  13409  lidrididd  13410  grpinvalem  13413  grpinva  13414  issgrp  13431  isnsgrp  13434  sgrpass  13436  sgrp1  13439  issgrpd  13440  sgrppropd  13441  ismndd  13465  mndpropd  13468  imasmnd2  13480  mnd1  13483  mnd1id  13484  ismhm  13489  mhmpropd  13494  mhmlin  13495  mhmeql  13520  isgrp  13534  grppropd  13545  isgrpd2e  13548  dfgrp2  13555  isgrpid2  13568  grpidd2  13569  grpinvfvalg  13570  grpinvpropdg  13603  grpidssd  13604  grpinvssd  13605  grpsubrcan  13609  dfgrp3mlem  13626  grplactcnv  13630  imasgrp2  13642  mhmlem  13646  mulgnn0p1  13665  mulgaddcom  13678  mulginvcom  13679  mulgneg2  13688  mulgnnass  13689  mulgnn0ass  13690  mulgass  13691  mhmmulg  13695  isghm  13775  ghmlin  13780  ghmeql  13799  iscmn  13825  cmnpropd  13827  iscmnd  13830  abladdsub4  13846  imasabl  13868  gsumfzconst  13873  isrng  13892  rngass  13897  rngdi  13898  rngdir  13899  rngpropd  13913  imasrng  13914  issrg  13923  srgmulgass  13947  srgpcomp  13948  srg1expzeq1  13953  isring  13958  iscrng2  13973  ringpropd  13996  ringinvnz1ne0  14007  mulgass2  14016  ring1  14017  imasring  14022  opprnegg  14041  dvdsrd  14052  dvreq1  14100  rhmmul  14122  isrhm2d  14123  rhmopp  14134  rhmunitinv  14136  islring  14150  rrgval  14220  unitrrg  14225  opprdomnbg  14232  islmod  14249  lmodlema  14250  islmodd  14251  lmodvsmmulgdi  14281  lmodprop2d  14306  rmodislmodlem  14308  rmodislmod  14309  rnglidlmsgrp  14455  rnglidlrng  14456  quscrng  14491  cnfldmulg  14534  cnfldexp  14535  gsumfzfsumlemm  14545  zndvds  14607  znf1o  14609  znunit  14617  psr1clfi  14646  txcnp  14939  cnmpt11  14951  cnmpt21  14959  cnmptcom  14966  isxms  15119  xmspropd  15145  bdmopn  15172  dvexp  15379  dvmptfsum  15393  rpcxpmul2  15581  wilthlem1  15648  mpodvdsmulf1o  15658  fsumdvdsmul  15659  perfect  15669  lgsne0  15711  gausslemma2d  15742  lgseisenlem2  15744  lgsquad2lem2  15755  2lgslem1a  15761  2lgslem1b  15762  usgredg2v  16016  wkslem1  16026  wkslem2  16027  iswlk  16029  nninffeq  16345