Theorem eqeq1d 2103

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

Hypothesis

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

Assertion

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

Proof of Theorem eqeq1d

Step	Hyp	Ref	Expression
1		eqeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqeq1 2101	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088

This theorem is referenced by:  rspcedeq1vd  2744  sbceq2g  2967  csbhypf  2980  csbiebt  2981  csbiebg  2984  dfss4st  3248  disjssun  3365  sneqrg  3628  preq12b  3636  preq12bg  3639  disji2  3860  iin0r  4025  opthg  4089  opeqsn  4103  unisucg  4265  opthreg  4400  tfisi  4430  dmsnopg  4936  relcoi1  4996  iotaeq  5022  iotabi  5023  fneq1  5136  fnun  5154  fnresdisj  5158  fnimadisj  5168  fnimaeq0  5169  sbcfng  5193  foeq1  5264  foco  5278  fveqeq2d  5348  fvelimab  5395  fvun1  5405  fvmptdv2  5428  fneqeql  5446  dffo3  5485  fvsng  5532  fconstfvm  5554  eufnfv  5564  f1veqaeq  5586  dff13f  5587  f1elima  5590  foeqcnvco  5607  f1eqcocnv  5608  acexmidlemab  5684  ovanraleqv  5714  eloprabga  5773  ovmpt2dv2  5816  ovi3  5819  ovelimab  5833  caovcang  5844  caovcan  5847  caovimo  5876  grprinvlem  5877  grpridd  5879  suppssfv  5890  suppssov1  5891  caofinvl  5915  op1stg  5959  op2ndg  5960  eqop  5985  reldm  5994  xporderlem  6034  tposfo2  6070  frec0g  6200  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecsuc  6210  nnm0r  6280  nnmord  6316  nnaordex  6326  nnawordex  6327  ereq1  6339  eqerlem  6363  mapsn  6487  endisj  6620  xpf1o  6640  mapxpen  6644  fidifsnen  6666  supelti  6777  updjudhcoinlf  6851  updjudhcoinrg  6852  updjud  6853  enomnilem  6881  finomni  6883  exmidomni  6885  fodjuomnilemres  6891  fodjuomni  6892  mkvprop  6901  fodjumkvlemres  6902  pm54.43  6915  exmidfodomrlemrALT  6926  addnidpig  6992  ltexpi  6993  dfplpq2  7010  dfmpq2  7011  recexnq  7046  recmulnqg  7047  ltexnqq  7064  halfnqq  7066  enq0tr  7090  nqnq0pi  7094  addnnnq0  7105  addlocpr  7192  ltexprlemru  7268  ltexpri  7269  lteupri  7273  prplnqu  7276  recexpr  7294  addsrpr  7388  mulsrpr  7389  00sr  7412  negexsr  7415  recexgt0sr  7416  srpospr  7425  prsrriota  7430  caucvgsrlemfv  7433  elrealeu  7464  axrnegex  7511  axprecex  7512  rereceu  7521  recriota  7522  nntopi  7526  axcaucvglemval  7529  axcaucvglemcau  7530  cnegexlem1  7754  cnegex  7757  cnegex2  7758  subval  7771  subadd  7782  subadd2  7783  subsub23  7784  addsubeq4  7794  subcan2  7804  negcon1  7831  subcan  7834  addrsub  7946  ltadd2  7994  ltordlem  8057  recexre  8152  recexap  8219  muleqadd  8234  receuap  8235  divvalap  8238  divmulap  8239  rec11ap  8274  zdiv  8933  uzin  9150  xaddval  9411  xnn0xadd0  9433  xnegdi  9434  xltadd1  9442  icc0r  9492  fznlem  9604  fseq1m1p1  9658  1fv  9699  fzon  9726  fvinim0ffz  9801  ioo0  9820  ico0  9822  ioc0  9823  flqbi  9846  divfl0  9852  modq0  9885  modqmuladdnn0  9924  addmodlteq  9954  frecuzrdgtcl  9968  frecuzrdgfunlem  9975  seq3f1olemstep  10051  seq3f1olemp  10052  seq3id  10058  seq3z  10061  mulreap  10413  rennim  10550  resqrexlemex  10573  rsqrmo  10575  resqrtcl  10577  rersqrtthlem  10578  sqrtsq2  10591  isumss  10934  fsum00  11005  telfsumo  11009  pwm1geoserap1  11051  absefib  11209  efieq1re  11210  divides  11225  dvdsval2  11226  nndivides  11230  dvds0lem  11233  dvds1lem  11234  dvds2lem  11235  negdvdsb  11239  muldvds1  11248  muldvds2  11249  dvdscmulr  11252  dvdsmulcr  11253  dvdstr  11260  dvdsabseq  11275  divconjdvds  11277  odd2np1lem  11299  odd2np1  11300  even2n  11301  oddm1even  11302  2tp1odd  11311  opeo  11324  omeo  11325  m1exp1  11328  divalgb  11352  gcdaddm  11402  gcdabs1  11407  bezout  11427  gcdmultiple  11436  gcdmultiplez  11437  rplpwr  11443  rppwr  11444  alginv  11456  algcvga  11460  algfx  11461  eucalgval2  11462  coprmdvds  11501  qredeq  11505  qredeu  11506  divgcdcoprm0  11510  divgcdcoprmex  11511  cncongr1  11512  rpexp  11559  rpexp12i  11561  cncongrprm  11563  qnumdenbi  11597  phival  11616  phicl2  11617  dfphi2  11623  phiprmpw  11625  phimullem  11628  hashgcdlem  11630  ntreq0  11984  ispsmet  12109  psmet0  12113  ismet  12130  isxmet  12131  xmeteq0  12145  metn0  12164  xmetres2  12165  xblss2ps  12190  xblss2  12191  xmseq0  12254  comet  12285  bdxmet  12287  cnmet  12309  peano4nninf  12610  nninfalllemn  12612  nninfalllem1  12613  nninfsellemdc  12616  nninfsellemeq  12620  nninfsellemqall  12621  nninfsellemeqinf  12622  nninfomnilem  12624  nninfomni  12625