Theorem eqeq12d 2220

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 2218	. 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 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  cdeqeq  2993  sbceqg  3109  csbing  3380  uniprg  3865  unisng  3867  intprg  3918  iununir  4011  csbopabg  4122  undifexmid  4237  exmidundif  4250  exmidundifim  4251  limeq  4424  onsucuni2  4612  ordpwsucexmid  4618  csbima12g  5043  dmsnsnsng  5160  cnvsng  5168  csbiotag  5264  fvmptf  5672  eqfnfv2f  5681  fvreseq  5683  fmptco  5746  fnressn  5770  fvsng  5780  cocan1  5856  cocan2  5857  fliftfun  5865  csbriotag  5912  oveqrspc2v  5971  csbov123g  5983  eqfnov  6052  ovmpos  6069  ov2gf  6070  ovmpodxf  6071  caovcomg  6102  caovassg  6105  caovcang  6108  caovcanrd  6110  caovcan  6111  caovdig  6121  caovdirg  6124  caovimo  6140  offveqb  6178  caofid0l  6185  caofid0r  6186  op1stg  6236  op2ndg  6237  f1o2ndf1  6314  tfrlem1  6394  tfrlem3ag  6395  tfrlem3a  6396  tfrlem5  6400  tfrlem9  6405  tfr0dm  6408  tfrlemiubacc  6416  tfrlemiex  6417  tfrlemi1  6418  tfr1onlem3ag  6423  tfr1onlemubacc  6432  tfr1onlemex  6433  tfr1onlemaccex  6434  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemubacc  6445  tfrcllemex  6446  tfrcllemaccex  6447  tfrcllemres  6448  tfrcldm  6449  tfri3  6453  rdg0g  6474  frecrdg  6494  nna0r  6564  nnacom  6570  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  ecopovtrn  6719  ecopovsymg  6721  ecopovtrng  6722  ecovcom  6729  ecovicom  6730  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  dom2lem  6863  ordiso2  7137  inl11  7167  updjud  7184  omp1eomlem  7196  difinfsnlem  7201  nnnninfeq  7230  nninfwlporlemd  7274  nninfwlpor  7276  nninfinfwlpo  7282  exmidfodomrlemrALT  7311  exmidaclem  7320  addcanpig  7447  mulcanpig  7448  mulcmpblnq  7481  mulpipqqs  7486  ordpipqqs  7487  mulidnq  7502  enq0sym  7545  nqnq0  7554  mulcmpblnq0  7557  distrnq0  7572  mulcomnq0  7573  addassnq0  7575  nq02m  7578  genipv  7622  cauappcvgprlemladd  7771  addcmpblnr  7852  0idsr  7880  1idsr  7881  axaddcom  7983  ax1rid  7990  ax0id  7991  rereceu  8002  axcaucvg  8013  mulrid  8069  readdcan  8212  cnegexlem1  8247  cnegexlem3  8249  addcan  8252  addcan2  8253  apti  8695  mulcanapd  8734  mulcanap2d  8735  div11ap  8773  divmuleqap  8790  conjmulap  8802  eqneg  8805  cnref1o  9772  fzsuc2  10201  fzprval  10204  fztpval  10205  qtri3or  10383  modqadd1  10506  modqmul1  10522  addmodlteq  10543  frec2uzrdg  10554  frecuzrdgg  10561  seq3val  10605  seqvalcd  10606  seq3fveq2  10620  seqfveq2g  10622  seqfveqg  10623  seq3fveq  10624  seq3feq  10625  seq3shft2  10626  seqshft2g  10627  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3caopr2  10638  seqcaopr2g  10639  iseqf1olemkle  10642  iseqf1olemklt  10643  iseqf1olemqk  10652  seq3f1olemqsum  10658  seq3f1olemstep  10659  seq3f1olemp  10660  seq3f1oleml  10661  seqf1oglem2a  10663  seqf1oglem2  10665  seqf1og  10666  seq3id  10670  seq3id2  10671  seq3homo  10672  seqhomog  10675  seqfeq4g  10676  mulexp  10723  expadd  10726  expmul  10729  modqexp  10811  nn0opth2d  10868  bcpasc  10911  hashennn  10925  hashen  10929  omgadd  10947  hashfzo  10967  hashfzp1  10969  hashxp  10971  hashfacen  10981  seq3coll  10987  eqs1  11082  swrdspsleq  11120  shftvalg  11147  shftval4g  11148  replim  11170  cjreb  11177  cjexp  11204  absexp  11390  recan  11420  minclpr  11548  mingeb  11553  sumeq2  11670  zsumdc  11695  fsum3  11698  fsumf1o  11701  fsum3cvg2  11705  fsumadd  11717  isummulc2  11737  fsum2d  11746  fsummulc2  11759  fsumconst  11765  modfsummod  11769  fsumparts  11781  fsumrelem  11782  fsumiun  11788  binom  11795  bcxmas  11800  isumshft  11801  isumnn0nn  11804  mertenslem2  11847  clim2prod  11850  prodfrecap  11857  prodeq2  11868  zproddc  11890  fprodseq  11894  fprodf1o  11899  prodsnf  11903  fprodfac  11926  fprodabs  11927  fprodconst  11931  fprod2d  11934  fprodrec  11940  fprodmodd  11952  efne0  11989  efexp  11993  demoivreALT  12085  moddvds  12110  bitsinv1  12273  gcddiv  12340  alginv  12369  algfx  12374  lcmneg  12396  lcmid  12402  lcmgcdeq  12405  divgcdcoprm0  12423  cncongr1  12425  cncongr2  12426  nn0gcdsq  12522  crth  12546  eulerthlema  12552  eulerthlemh  12553  pythagtriplem1  12588  pcqmul  12626  pcexp  12632  pcneg  12648  pcmpt  12666  pcfac  12673  1arith  12690  setscomd  12873  ercpbllemg  13162  mgmidmo  13204  mgmlrid  13211  lidrideqd  13213  lidrididd  13214  grpinvalem  13217  grpinva  13218  issgrp  13235  isnsgrp  13238  sgrpass  13240  sgrp1  13243  issgrpd  13244  sgrppropd  13245  ismndd  13269  mndpropd  13272  imasmnd2  13284  mnd1  13287  mnd1id  13288  ismhm  13293  mhmpropd  13298  mhmlin  13299  mhmeql  13324  isgrp  13338  grppropd  13349  isgrpd2e  13352  dfgrp2  13359  isgrpid2  13372  grpidd2  13373  grpinvfvalg  13374  grpinvpropdg  13407  grpidssd  13408  grpinvssd  13409  grpsubrcan  13413  dfgrp3mlem  13430  grplactcnv  13434  imasgrp2  13446  mhmlem  13450  mulgnn0p1  13469  mulgaddcom  13482  mulginvcom  13483  mulgneg2  13492  mulgnnass  13493  mulgnn0ass  13494  mulgass  13495  mhmmulg  13499  isghm  13579  ghmlin  13584  ghmeql  13603  iscmn  13629  cmnpropd  13631  iscmnd  13634  abladdsub4  13650  imasabl  13672  gsumfzconst  13677  isrng  13696  rngass  13701  rngdi  13702  rngdir  13703  rngpropd  13717  imasrng  13718  issrg  13727  srgmulgass  13751  srgpcomp  13752  srg1expzeq1  13757  isring  13762  iscrng2  13777  ringpropd  13800  ringinvnz1ne0  13811  mulgass2  13820  ring1  13821  imasring  13826  opprnegg  13845  dvdsrd  13856  dvreq1  13904  rhmmul  13926  isrhm2d  13927  rhmopp  13938  rhmunitinv  13940  islring  13954  rrgval  14024  unitrrg  14029  opprdomnbg  14036  islmod  14053  lmodlema  14054  islmodd  14055  lmodvsmmulgdi  14085  lmodprop2d  14110  rmodislmodlem  14112  rmodislmod  14113  rnglidlmsgrp  14259  rnglidlrng  14260  quscrng  14295  cnfldmulg  14338  cnfldexp  14339  gsumfzfsumlemm  14349  zndvds  14411  znf1o  14413  znunit  14421  psr1clfi  14450  txcnp  14743  cnmpt11  14755  cnmpt21  14763  cnmptcom  14770  isxms  14923  xmspropd  14949  bdmopn  14976  dvexp  15183  dvmptfsum  15197  rpcxpmul2  15385  wilthlem1  15452  mpodvdsmulf1o  15462  fsumdvdsmul  15463  perfect  15473  lgsne0  15515  gausslemma2d  15546  lgseisenlem2  15548  lgsquad2lem2  15559  2lgslem1a  15565  2lgslem1b  15566  nninffeq  15957