Theorem eqeq12d 2114

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	⊢ (𝜑 → 𝐴 = 𝐵)
eqeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eqeq12d	⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Proof of Theorem eqeq12d

Step	Hyp	Ref	Expression
1		eqeq12d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		eqeq12 2112	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2anc 406	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299

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 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  cdeqeq  2857  sbceqg  2969  csbing  3230  uniprg  3698  unisng  3700  intprg  3751  iununir  3842  csbopabg  3946  undifexmid  4057  exmidundif  4067  exmidundifim  4068  limeq  4237  onsucuni2  4417  ordpwsucexmid  4423  csbima12g  4836  dmsnsnsng  4952  cnvsng  4960  csbiotag  5052  fvmptf  5445  eqfnfv2f  5454  fvreseq  5456  fmptco  5518  fnressn  5538  fvsng  5548  cocan1  5620  cocan2  5621  fliftfun  5629  csbriotag  5674  csbov123g  5741  eqfnov  5809  ovmpos  5826  ov2gf  5827  ovmpodxf  5828  caovcomg  5858  caovassg  5861  caovcang  5864  caovcanrd  5866  caovcan  5867  caovdig  5877  caovdirg  5880  caovimo  5896  grprinvlem  5897  grprinvd  5898  offveqb  5932  op1stg  5979  op2ndg  5980  f1o2ndf1  6055  tfrlem1  6135  tfrlem3ag  6136  tfrlem3a  6137  tfrlem5  6141  tfrlem9  6146  tfr0dm  6149  tfrlemiubacc  6157  tfrlemiex  6158  tfrlemi1  6159  tfr1onlem3ag  6164  tfr1onlemubacc  6173  tfr1onlemex  6174  tfr1onlemaccex  6175  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllemubacc  6186  tfrcllemex  6187  tfrcllemaccex  6188  tfrcllemres  6189  tfrcldm  6190  tfri3  6194  rdg0g  6215  frecrdg  6235  nna0r  6304  nnacom  6310  nnaass  6311  nndi  6312  nnmass  6313  nnmsucr  6314  nnmcom  6315  ecopovtrn  6456  ecopovsymg  6458  ecopovtrng  6459  ecovcom  6466  ecovicom  6467  ecovass  6468  ecoviass  6469  ecovdi  6470  ecovidi  6471  dom2lem  6596  ordiso2  6835  inl11  6865  updjud  6882  omp1eomlem  6894  difinfsnlem  6899  exmidfodomrlemrALT  6968  addcanpig  7043  mulcanpig  7044  mulcmpblnq  7077  mulpipqqs  7082  ordpipqqs  7083  mulidnq  7098  enq0sym  7141  nqnq0  7150  mulcmpblnq0  7153  distrnq0  7168  mulcomnq0  7169  addassnq0  7171  nq02m  7174  genipv  7218  cauappcvgprlemladd  7367  addcmpblnr  7435  0idsr  7463  1idsr  7464  axaddcom  7555  ax1rid  7562  ax0id  7563  rereceu  7574  axcaucvg  7585  mulid1  7635  readdcan  7773  cnegexlem1  7808  cnegexlem3  7810  addcan  7813  addcan2  7814  apti  8250  mulcanapd  8283  mulcanap2d  8284  div11ap  8321  divmuleqap  8338  conjmulap  8350  eqneg  8353  cnref1o  9290  fzsuc2  9700  fzprval  9703  fztpval  9704  qtri3or  9861  modqadd1  9975  modqmul1  9991  addmodlteq  10012  frec2uzrdg  10023  frecuzrdgg  10030  seq3val  10072  seqvalcd  10073  seq3fveq2  10083  seq3fveq  10085  seq3feq  10086  seq3shft2  10087  seq3split  10093  seq3caopr3  10095  seq3caopr2  10096  iseqf1olemkle  10098  iseqf1olemklt  10099  iseqf1olemqk  10108  seq3f1olemqsum  10114  seq3f1olemstep  10115  seq3f1olemp  10116  seq3f1oleml  10117  seq3id  10122  seq3id2  10123  seq3homo  10124  mulexp  10173  expadd  10176  expmul  10179  nn0opth2d  10310  bcpasc  10353  hashennn  10367  hashen  10371  omgadd  10389  hashfzo  10409  hashfzp1  10411  hashxp  10413  hashfacen  10420  seq3coll  10426  shftvalg  10449  shftval4g  10450  replim  10472  cjreb  10479  cjexp  10506  absexp  10691  recan  10721  minclpr  10847  sumeq2  10967  zsumdc  10992  fsum3  10995  fsumf1o  10998  fsum3cvg2  11002  fsumadd  11014  isummulc2  11034  fsum2d  11043  fsummulc2  11056  fsumconst  11062  modfsummod  11066  fsumparts  11078  fsumrelem  11079  fsumiun  11085  binom  11092  bcxmas  11097  isumshft  11098  isumnn0nn  11101  mertenslem2  11144  efne0  11182  efexp  11186  demoivreALT  11277  moddvds  11297  gcddiv  11500  alginv  11521  algfx  11526  lcmneg  11548  lcmid  11554  lcmgcdeq  11557  divgcdcoprm0  11575  cncongr1  11577  cncongr2  11578  nn0gcdsq  11670  crth  11692  txcnp  12221  cnmpt11  12233  cnmpt21  12241  cnmptcom  12248  isxms  12379  xmspropd  12405  bdmopn  12432  nninfalllemn  12786  nninffeq  12800