Theorem eqeq12d 2054

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 2052	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	1, 2, 3	syl2anc 391	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  cdeqeq  2759  sbceqg  2866  csbing  3144  uniprg  3595  unisng  3597  intprg  3648  iununir  3738  csbopabg  3835  limeq  4114  onsucuni2  4288  ordpwsucexmid  4294  csbima12g  4686  dmsnsnsng  4798  cnvsng  4806  csbiotag  4895  fvmptf  5263  eqfnfv2f  5269  fvreseq  5271  fmptco  5330  fnressn  5349  fvsng  5359  cocan1  5427  cocan2  5428  fliftfun  5436  csbriotag  5480  csbov123g  5543  eqfnov  5607  ovmpt2s  5624  ov2gf  5625  ovmpt2dxf  5626  caovcomg  5656  caovassg  5659  caovcang  5662  caovcanrd  5664  caovcan  5665  caovdig  5675  caovdirg  5678  caovimo  5694  grprinvlem  5695  grprinvd  5696  offveqb  5730  op1stg  5777  op2ndg  5778  f1o2ndf1  5849  tfrlem1  5923  tfrlem3ag  5924  tfrlem3a  5925  tfrlem5  5930  tfrlem9  5935  tfr0  5937  tfrlemiubacc  5944  tfrlemiex  5945  tfrlemi1  5946  tfri3  5953  rdg0g  5975  frecrdg  5992  nna0r  6057  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  ecopovtrn  6203  ecopovsymg  6205  ecopovtrng  6206  ecovcom  6213  ecovicom  6214  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  dom2lem  6252  ordiso2  6357  addcanpig  6432  mulcanpig  6433  mulcmpblnq  6466  mulpipqqs  6471  ordpipqqs  6472  mulidnq  6487  enq0sym  6530  nqnq0  6539  mulcmpblnq0  6542  distrnq0  6557  mulcomnq0  6558  addassnq0  6560  nq02m  6563  genipv  6607  cauappcvgprlemladd  6756  addcmpblnr  6824  0idsr  6852  1idsr  6853  axaddcom  6944  ax1rid  6951  ax0id  6952  rereceu  6963  axcaucvg  6974  mulid1  7024  readdcan  7153  cnegexlem1  7186  cnegexlem3  7188  addcan  7191  addcan2  7192  apti  7613  mulcanapd  7642  mulcanap2d  7643  div11ap  7677  divmuleqap  7693  conjmulap  7705  eqneg  7708  cnref1o  8582  fzsuc2  8941  fzprval  8944  fztpval  8945  qtri3or  9098  frec2uzrdg  9195  iseqss  9226  iseqfveq2  9228  iseqfveq  9230  iseqfeq  9231  iseqshft2  9232  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqid  9247  iseqhomo  9248  mulexp  9294  expadd  9297  expmul  9300  shftvalg  9437  shftval4g  9438  replim  9459  cjreb  9466  cjexp  9493  absexp  9675  recan  9705  ialginv  9886  ialgfx  9891