Theorem eqeq1d 2045

Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eqeq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eqeq1d	⊢ (φ → (A = 𝐶 ↔ B = 𝐶))

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 ⊢ (φ → A = B)
2		eqeq1 2043	. 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))
3	1, 2	syl 14	1 ⊢ (φ → (A = 𝐶 ↔ B = 𝐶))

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

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  sbceq2g  2866  csbhypf  2879  csbiebt  2880  csbiebg  2883  disjssun  3279  sneqrg  3524  preq12b  3532  preq12bg  3535  iin0r  3913  opthg  3966  opeqsn  3980  unisucg  4117  opthreg  4234  tfisi  4253  dmsnopg  4735  relcoi1  4792  iotaeq  4818  iotabi  4819  fneq1  4930  fnun  4948  fnresdisj  4952  fnimadisj  4962  fnimaeq0  4963  sbcfng  4987  foeq1  5045  foco  5059  fvelimab  5172  fvun1  5182  fvmptdv2  5203  fneqeql  5218  dffo3  5257  fvsng  5302  fconstfvm  5322  eufnfv  5332  f1veqaeq  5351  dff13f  5352  f1elima  5355  foeqcnvco  5373  f1eqcocnv  5374  acexmidlemab  5449  eloprabga  5533  ovmpt2dv2  5576  ovi3  5579  ovelimab  5593  caovcang  5604  caovcan  5607  caovimo  5636  grprinvlem  5637  grpridd  5639  suppssfv  5650  suppssov1  5651  caofinvl  5675  op1stg  5719  op2ndg  5720  eqop  5745  reldm  5754  xporderlem  5793  tposfo2  5823  frec0g  5922  frecsuclem3  5929  frecsuc  5930  nnm0r  5997  nnmord  6026  nnaordex  6036  nnawordex  6037  ereq1  6049  eqerlem  6073  endisj  6234  addnidpig  6320  ltexpi  6321  dfplpq2  6338  dfmpq2  6339  recexnq  6374  recmulnqg  6375  ltexnqq  6391  halfnqq  6393  enq0tr  6416  nqnq0pi  6420  addnnnq0  6431  addlocpr  6518  ltexprlemru  6585  ltexpri  6586  recexpr  6609  addsrpr  6653  mulsrpr  6654  00sr  6677  negexsr  6680  recexgt0sr  6681  axrnegex  6743  axprecex  6744  cnegexlem1  6963  cnegex  6966  cnegex2  6967  subval  6980  subadd  6991  subadd2  6992  subsub23  6993  addsubeq4  7003  subcan2  7012  negcon1  7039  subcan  7042  ltadd2  7192  recexre  7342  recexap  7396  muleqadd  7411  receuap  7412  divvalap  7415  divmulap  7416  rec11ap  7448  zdiv  8084  uzin  8261  icc0r  8545  fznlem  8655  fseq1m1p1  8707  1fv  8746  fzon  8772  frecuzrdgfn  8859  mulreap  9072  rennim  9191