Theorem eqeq12d 2127

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 2125	. 2 |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
4	1, 2, 3	syl2anc 406	1 |- ( ph -> ( A = C <-> B = D ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1312

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106

This theorem is referenced by:  cdeqeq  2871  sbceqg  2983  csbing  3247  uniprg  3715  unisng  3717  intprg  3768  iununir  3860  csbopabg  3964  undifexmid  4075  exmidundif  4087  exmidundifim  4088  limeq  4257  onsucuni2  4437  ordpwsucexmid  4443  csbima12g  4856  dmsnsnsng  4972  cnvsng  4980  csbiotag  5072  fvmptf  5465  eqfnfv2f  5474  fvreseq  5476  fmptco  5538  fnressn  5558  fvsng  5568  cocan1  5640  cocan2  5641  fliftfun  5649  csbriotag  5694  csbov123g  5761  eqfnov  5829  ovmpos  5846  ov2gf  5847  ovmpodxf  5848  caovcomg  5878  caovassg  5881  caovcang  5884  caovcanrd  5886  caovcan  5887  caovdig  5897  caovdirg  5900  caovimo  5916  grprinvlem  5917  grprinvd  5918  offveqb  5952  op1stg  5999  op2ndg  6000  f1o2ndf1  6076  tfrlem1  6156  tfrlem3ag  6157  tfrlem3a  6158  tfrlem5  6162  tfrlem9  6167  tfr0dm  6170  tfrlemiubacc  6178  tfrlemiex  6179  tfrlemi1  6180  tfr1onlem3ag  6185  tfr1onlemubacc  6194  tfr1onlemex  6195  tfr1onlemaccex  6196  tfrcllemsucaccv  6202  tfrcllembxssdm  6204  tfrcllemubacc  6207  tfrcllemex  6208  tfrcllemaccex  6209  tfrcllemres  6210  tfrcldm  6211  tfri3  6215  rdg0g  6236  frecrdg  6256  nna0r  6325  nnacom  6331  nnaass  6332  nndi  6333  nnmass  6334  nnmsucr  6335  nnmcom  6336  ecopovtrn  6477  ecopovsymg  6479  ecopovtrng  6480  ecovcom  6487  ecovicom  6488  ecovass  6489  ecoviass  6490  ecovdi  6491  ecovidi  6492  dom2lem  6617  ordiso2  6869  inl11  6899  updjud  6916  omp1eomlem  6928  difinfsnlem  6933  exmidfodomrlemrALT  7003  exmidaclem  7008  addcanpig  7083  mulcanpig  7084  mulcmpblnq  7117  mulpipqqs  7122  ordpipqqs  7123  mulidnq  7138  enq0sym  7181  nqnq0  7190  mulcmpblnq0  7193  distrnq0  7208  mulcomnq0  7209  addassnq0  7211  nq02m  7214  genipv  7258  cauappcvgprlemladd  7407  addcmpblnr  7475  0idsr  7503  1idsr  7504  axaddcom  7598  ax1rid  7605  ax0id  7606  rereceu  7617  axcaucvg  7628  mulid1  7680  readdcan  7818  cnegexlem1  7853  cnegexlem3  7855  addcan  7858  addcan2  7859  apti  8295  mulcanapd  8328  mulcanap2d  8329  div11ap  8366  divmuleqap  8383  conjmulap  8395  eqneg  8398  cnref1o  9335  fzsuc2  9745  fzprval  9748  fztpval  9749  qtri3or  9906  modqadd1  10020  modqmul1  10036  addmodlteq  10057  frec2uzrdg  10068  frecuzrdgg  10075  seq3val  10117  seqvalcd  10118  seq3fveq2  10128  seq3fveq  10130  seq3feq  10131  seq3shft2  10132  seq3split  10138  seq3caopr3  10140  seq3caopr2  10141  iseqf1olemkle  10143  iseqf1olemklt  10144  iseqf1olemqk  10153  seq3f1olemqsum  10159  seq3f1olemstep  10160  seq3f1olemp  10161  seq3f1oleml  10162  seq3id  10167  seq3id2  10168  seq3homo  10169  mulexp  10218  expadd  10221  expmul  10224  nn0opth2d  10355  bcpasc  10398  hashennn  10412  hashen  10416  omgadd  10434  hashfzo  10454  hashfzp1  10456  hashxp  10458  hashfacen  10465  seq3coll  10471  shftvalg  10494  shftval4g  10495  replim  10517  cjreb  10524  cjexp  10551  absexp  10736  recan  10766  minclpr  10893  sumeq2  11013  zsumdc  11038  fsum3  11041  fsumf1o  11044  fsum3cvg2  11048  fsumadd  11060  isummulc2  11080  fsum2d  11089  fsummulc2  11102  fsumconst  11108  modfsummod  11112  fsumparts  11124  fsumrelem  11125  fsumiun  11131  binom  11138  bcxmas  11143  isumshft  11144  isumnn0nn  11147  mertenslem2  11190  efne0  11228  efexp  11232  demoivreALT  11323  moddvds  11343  gcddiv  11546  alginv  11567  algfx  11572  lcmneg  11594  lcmid  11600  lcmgcdeq  11603  divgcdcoprm0  11621  cncongr1  11623  cncongr2  11624  nn0gcdsq  11716  crth  11738  txcnp  12275  cnmpt11  12287  cnmpt21  12295  cnmptcom  12302  isxms  12433  xmspropd  12459  bdmopn  12486  nninfalllemn  12879  nninffeq  12893