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  6417  nqnq0pi  6421  addnnnq0  6432  addlocpr  6519  ltexprlemru  6586  ltexpri  6587  recexpr  6610  addsrpr  6673  mulsrpr  6674  00sr  6697  negexsr  6700  recexgt0sr  6701  axrnegex  6763  axprecex  6764  cnegexlem1  6983  cnegex  6986  cnegex2  6987  subval  7000  subadd  7011  subadd2  7012  subsub23  7013  addsubeq4  7023  subcan2  7032  negcon1  7059  subcan  7062  ltadd2  7212  recexre  7362  recexap  7416  muleqadd  7431  receuap  7432  divvalap  7435  divmulap  7436  rec11ap  7468  zdiv  8104  uzin  8281  icc0r  8565  fznlem  8675  fseq1m1p1  8727  1fv  8766  fzon  8792  frecuzrdgfn  8879  mulreap  9092  rennim  9211