Theorem eqeq12d 2095

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

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  cdeqeq  2810  sbceqg  2922  csbing  3173  uniprg  3616  unisng  3618  intprg  3669  iununir  3759  csbopabg  3856  limeq  4132  onsucuni2  4307  ordpwsucexmid  4313  csbima12g  4706  dmsnsnsng  4818  cnvsng  4826  csbiotag  4915  fvmptf  5284  eqfnfv2f  5290  fvreseq  5292  fmptco  5351  fnressn  5370  fvsng  5380  cocan1  5447  cocan2  5448  fliftfun  5456  csbriotag  5500  csbov123g  5563  eqfnov  5627  ovmpt2s  5644  ov2gf  5645  ovmpt2dxf  5646  caovcomg  5676  caovassg  5679  caovcang  5682  caovcanrd  5684  caovcan  5685  caovdig  5695  caovdirg  5698  caovimo  5714  grprinvlem  5715  grprinvd  5716  offveqb  5750  op1stg  5797  op2ndg  5798  f1o2ndf1  5869  tfrlem1  5946  tfrlem3ag  5947  tfrlem3a  5948  tfrlem5  5953  tfrlem9  5958  tfr0  5960  tfrlemiubacc  5967  tfrlemiex  5968  tfrlemi1  5969  tfri3  5976  rdg0g  5998  frecrdg  6015  nna0r  6080  nnacom  6086  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  nnmcom  6091  ecopovtrn  6226  ecopovsymg  6228  ecopovtrng  6229  ecovcom  6236  ecovicom  6237  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  dom2lem  6275  ordiso2  6446  addcanpig  6524  mulcanpig  6525  mulcmpblnq  6558  mulpipqqs  6563  ordpipqqs  6564  mulidnq  6579  enq0sym  6622  nqnq0  6631  mulcmpblnq0  6634  distrnq0  6649  mulcomnq0  6650  addassnq0  6652  nq02m  6655  genipv  6699  cauappcvgprlemladd  6848  addcmpblnr  6916  0idsr  6944  1idsr  6945  axaddcom  7036  ax1rid  7043  ax0id  7044  rereceu  7055  axcaucvg  7066  mulid1  7116  readdcan  7248  cnegexlem1  7283  cnegexlem3  7285  addcan  7288  addcan2  7289  apti  7722  mulcanapd  7751  mulcanap2d  7752  div11ap  7788  divmuleqap  7805  conjmulap  7817  eqneg  7820  cnref1o  8733  fzsuc2  9096  fzprval  9099  fztpval  9100  qtri3or  9252  modqadd1  9363  modqmul1  9379  addmodlteq  9400  frec2uzrdg  9411  iseqss  9446  iseqfveq2  9448  iseqfveq  9450  iseqfeq  9451  iseqshft2  9452  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqid  9467  iseqhomo  9468  mulexp  9515  expadd  9518  expmul  9521  nn0opth2d  9650  bcpasc  9693  shftvalg  9724  shftval4g  9725  replim  9746  cjreb  9753  cjexp  9780  absexp  9965  recan  9995  moddvds  10204  gcddiv  10408  ialginv  10429  ialgfx  10434  lcmneg  10456  lcmid  10462  lcmgcdeq  10465  divgcdcoprm0  10483  cncongr1  10485  cncongr2  10486