Theorem eqeq2d 2096

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

Hypothesis

Ref	Expression
eqeq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

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

Proof of Theorem eqeq2d

Step	Hyp	Ref	Expression
1		eqeq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq2 2094	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1287

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-cleq 2078

This theorem is referenced by:  eqtrd  2117  eq2tri  2144  rspcedeq2vd  2723  sbceq1g  2940  euabsn  3495  absneu  3497  preq12bg  3600  cbvopab  3884  cbvopab1  3886  cbvopab2  3887  cbvopab1s  3888  cbvopab2v  3890  mpteq12f  3893  cbvmptf  3907  cbvmpt  3908  opth  4038  eqvinop  4044  moop2  4052  euotd  4055  eusvnf  4249  reusv3i  4255  nlimsucg  4355  nn0suc  4392  opelxp  4440  elvvv  4469  relop  4554  elrnmpt1s  4653  elrnmpt1  4654  elsnres  4716  elxp4  4884  elxp5  4885  relresfld  4926  iotajust  4945  iota1  4960  iota2df  4970  funopg  5013  funcnvuni  5048  fun11iun  5237  funcocnv2  5241  nfvres  5300  ssimaex  5328  fvmptg  5343  fvmptdf  5353  fvopab6  5359  fmptco  5427  fsng  5433  foco2  5494  elabrex  5498  abrexco  5499  f1veqaeq  5509  dff13f  5510  f1ocnvfv  5519  f1ocnvfvb  5520  fcofo  5524  fliftfun  5536  fliftval  5540  f1oiso2  5567  riota5f  5593  oprabid  5638  rspceov  5648  dfoprab2  5653  mpt2eq123dva  5667  mpt2eq3dva  5670  cbvoprab1  5677  cbvoprab2  5678  cbvoprab12  5679  cbvmpt2x  5683  mpt2mptx  5696  ovmpt2s  5725  ovmpt2df  5733  ovmpt2dv2  5735  ovi3  5738  ov6g  5739  fnrnov  5747  foov  5748  caovcang  5763  caovcan  5766  f1opw2  5807  opabex3d  5849  opabex3  5850  fo1st  5885  fo2nd  5886  elxp6  5897  op1steq  5906  dfoprab4f  5920  fmpt2x  5927  df1st2  5941  df2nd2  5942  xporderlem  5953  cnvoprab  5956  f1od2  5957  brtpos2  5970  dftpos4  5982  tposfn2  5985  recseq  6025  tfr1onlemaccex  6067  tfrcllemaccex  6080  frecabcl  6118  frecsuc  6126  nna0r  6193  eqerlem  6275  qseq2  6293  ecelqsg  6297  snec  6305  qsinxp  6320  ecoptocl  6331  eroveu  6335  th3qlem1  6346  th3qlem2  6347  th3q  6349  mapsncnv  6404  en1  6468  mapsnen  6480  xpsnen  6489  xpassen  6498  xpf1o  6512  mapen  6514  mapxpen  6516  fidifsnen  6538  ac6sfi  6566  undifdc  6586  djuf1olem  6689  djur  6701  updjud  6717  fodjuomnilemdc  6743  fodjuomnilem0  6746  fodjuomni  6748  exmidfodomrlemeldju  6769  exmidfodomrlemreseldju  6770  dfplpq2  6857  dfmpq2  6858  enqbreq2  6860  enq0sym  6935  enq0ref  6936  enq0tr  6937  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  mulnnnq0  6953  nqnq0a  6957  nqnq0m  6958  nq0a0  6960  prarloclemcalc  7005  genipv  7012  genpassl  7027  genpassu  7028  addcomprg  7081  mulcomprg  7083  distrlem1prl  7085  distrlem1pru  7086  distrlem5prl  7089  distrlem5pru  7090  1idprl  7093  1idpru  7094  recexprlem1ssl  7136  recexprlem1ssu  7137  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  elreal  7310  axcnre  7360  axcaucvglemval  7376  negeu  7617  subeq0  7652  apreap  8005  apreim  8021  divmulap3  8083  diveqap0  8088  diveqap1  8111  nn0ind-raph  8796  elq  9039  zq  9043  cnref1o  9065  iccf1o  9353  fzen  9389  fseq1m1p1  9439  fzm1  9444  modqmuladd  9701  modqmuladdnn0  9703  modfzo0difsn  9730  nn0ennn  9768  iseqid2  9843  ibcval5  10067  fihashen1  10103  shftlem  10146  shftfvalg  10148  shftfval  10151  negfi  10552  sumeq2  10638  isummo  10662  fisum  10665  moddvds  10680  dvdsnegb  10688  dvdsabseq  10723  dvdsmod  10738  odd2np1lem  10747  odd2np1  10748  opeo  10772  omeo  10773  divalglemnn  10793  divalglemeunn  10796  divalglemex  10797  divalglemeuneg  10798  bezoutlemnewy  10860  bezoutlema  10863  bezoutlemb  10864  bezoutlemex  10865  bezoutlemaz  10867  bezoutlembz  10868  eucalglt  10914  qredeq  10953  qredeu  10954  divgcdcoprm0  10958  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  qnumdenbi  11045  hashgcdlem  11078  evenennn  11081  bj-nn0suc0  11283  bj-inf2vnlem1  11303  bj-nn0sucALT  11311