Theorem eqeq1d 2026

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 2024	. 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))
3	1, 2	syl 14	1 ⊢ (φ → (A = 𝐶 ↔ B = 𝐶))

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

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 1312  ax-gen 1314  ax-4 1377  ax-17 1396  ax-ext 2000

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

This theorem is referenced by:  sbceq2g  2845  csbhypf  2858  csbiebt  2859  csbiebg  2862  disjssun  3258  sneqrg  3503  preq12b  3511  preq12bg  3514  iin0r  3892  opthg  3945  opeqsn  3959  unisucg  4096  opthreg  4214  tfisi  4233  dmsnopg  4715  relcoi1  4772  iotaeq  4798  iotabi  4799  fneq1  4909  fnun  4927  fnresdisj  4931  fnimadisj  4941  fnimaeq0  4942  sbcfng  4966  foeq1  5023  foco  5037  fvelimab  5150  fvun1  5160  fvmptdv2  5181  fneqeql  5196  dffo3  5235  fvsng  5280  fconstfvm  5300  eufnfv  5310  f1veqaeq  5329  dff13f  5330  f1elima  5333  foeqcnvco  5351  f1eqcocnv  5352  acexmidlemab  5426  eloprabga  5510  ovmpt2dv2  5553  ovi3  5556  ovelimab  5570  caovcang  5581  caovcan  5584  caovimo  5613  grprinvlem  5614  grpridd  5616  suppssfv  5627  suppssov1  5628  caofinvl  5652  op1stg  5696  op2ndg  5697  eqop  5722  reldm  5731  xporderlem  5770  tposfo2  5800  frec0g  5898  frecsuclem3  5902  frecsuc  5903  nnm0r  5969  nnmord  5997  nnaordex  6007  nnawordex  6008  ereq1  6020  eqerlem  6044  addnidpig  6190  ltexpi  6191  dfplpq2  6207  dfmpq2  6208  recex  6243  recmulnqg  6244  ltexnqq  6260  halfnqq  6261  enq0tr  6283  nqnq0pi  6287  addnnnq0  6298  addlocpr  6385  ltexprlemru  6443  ltexpri  6444  recexpr  6466  addsrpr  6486  mulsrpr  6487  00sr  6510  negexsr  6513  recexsrlem  6514  axrnegex  6567  axprecex  6568  cnegexlem1  6773  cnegex  6776  cnegex2  6777  subval  6790  subadd  6801  subadd2  6802  subsub23  6803  addsubeq4  6813  subcan2  6822  negcon1  6849  subcan  6852  ltadd2  7002