Theorem eqeq1d 2149

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 2147	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  rspcedeq1vd  2802  sbceq2g  3029  csbhypf  3043  csbiebt  3044  csbiebg  3047  dfss4st  3314  disjssun  3431  sneqrg  3697  preq12b  3705  preq12bg  3708  disji2  3930  iin0r  4101  opthg  4168  opeqsn  4182  unisucg  4344  opthreg  4479  tfisi  4509  dmsnopg  5018  relcoi1  5078  iotaeq  5104  iotabi  5105  fneq1  5219  fnun  5237  fnresdisj  5241  fnimadisj  5251  fnimaeq0  5252  sbcfng  5278  foeq1  5349  foco  5363  fveqeq2d  5437  fvelimab  5485  fvun1  5495  fvmptdv2  5518  fneqeql  5536  dffo3  5575  fvsng  5624  fconstfvm  5646  eufnfv  5656  f1veqaeq  5678  dff13f  5679  f1elima  5682  foeqcnvco  5699  f1eqcocnv  5700  acexmidlemab  5776  ovanraleqv  5806  eloprabga  5866  ovmpodv2  5912  ovi3  5915  ovelimab  5929  caovcang  5940  caovcan  5943  caovimo  5972  grprinvlem  5973  grpridd  5975  suppssfv  5986  suppssov1  5987  caofinvl  6012  op1stg  6056  op2ndg  6057  eqop  6083  reldm  6092  xporderlem  6136  tposfo2  6172  frec0g  6302  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  nnm0r  6383  nnmord  6421  nnaordex  6431  nnawordex  6432  ereq1  6444  eqerlem  6468  mapsn  6592  endisj  6726  xpf1o  6746  mapxpen  6750  fidifsnen  6772  supelti  6897  updjudhcoinlf  6973  updjudhcoinrg  6974  updjud  6975  omp1eomlem  6987  difinfsnlem  6992  enomnilem  7018  finomni  7020  exmidomni  7022  fodjuomnilemres  7028  fodjuomni  7029  ismkvnex  7037  mkvprop  7040  fodjumkvlemres  7041  enmkvlem  7043  enwomnilem  7050  pm54.43  7063  exmidfodomrlemrALT  7076  cc2lem  7098  addnidpig  7168  ltexpi  7169  dfplpq2  7186  dfmpq2  7187  recexnq  7222  recmulnqg  7223  ltexnqq  7240  halfnqq  7242  enq0tr  7266  nqnq0pi  7270  addnnnq0  7281  addlocpr  7368  ltexprlemru  7444  ltexpri  7445  lteupri  7449  prplnqu  7452  recexpr  7470  addsrpr  7577  mulsrpr  7578  00sr  7601  negexsr  7604  recexgt0sr  7605  srpospr  7615  prsrriota  7620  caucvgsrlemfv  7623  map2psrprg  7637  elrealeu  7661  axrnegex  7711  axprecex  7712  rereceu  7721  recriota  7722  nntopi  7726  axcaucvglemval  7729  axcaucvglemcau  7730  cnegexlem1  7961  cnegex  7964  cnegex2  7965  subval  7978  subadd  7989  subadd2  7990  subsub23  7991  addsubeq4  8001  subcan2  8011  negcon1  8038  subcan  8041  addrsub  8157  ltadd2  8205  ltordlem  8268  recexre  8364  recexap  8438  muleqadd  8453  receuap  8454  divvalap  8458  divmulap  8459  rec11ap  8494  zdiv  9163  uzin  9382  xaddval  9658  xnn0xadd0  9680  xnegdi  9681  xltadd1  9689  icc0r  9739  fznlem  9852  fseq1m1p1  9906  1fv  9947  fzon  9974  fvinim0ffz  10049  ioo0  10068  ico0  10070  ioc0  10071  flqbi  10094  divfl0  10100  modq0  10133  modqmuladdnn0  10172  addmodlteq  10202  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  seq3f1olemstep  10305  seq3f1olemp  10306  seq3id  10312  seq3z  10315  mulreap  10668  rennim  10806  resqrexlemex  10829  rsqrmo  10831  resqrtcl  10833  rersqrtthlem  10834  sqrtsq2  10847  isumss  11192  fsum00  11263  telfsumo  11267  pwm1geoserap1  11309  absefib  11513  efieq1re  11514  divides  11531  dvdsval2  11532  nndivides  11536  dvds0lem  11539  dvds1lem  11540  dvds2lem  11541  negdvdsb  11545  muldvds1  11554  muldvds2  11555  dvdscmulr  11558  dvdsmulcr  11559  dvdstr  11566  dvdsabseq  11581  divconjdvds  11583  odd2np1lem  11605  odd2np1  11606  even2n  11607  oddm1even  11608  2tp1odd  11617  opeo  11630  omeo  11631  m1exp1  11634  divalgb  11658  gcdaddm  11708  gcdabs1  11713  bezout  11735  gcdmultiple  11744  gcdmultiplez  11745  rplpwr  11751  rppwr  11752  alginv  11764  algcvga  11768  algfx  11769  eucalgval2  11770  coprmdvds  11809  qredeq  11813  qredeu  11814  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  rpexp  11867  rpexp12i  11869  cncongrprm  11871  qnumdenbi  11906  phival  11925  phicl2  11926  dfphi2  11932  phiprmpw  11934  phimullem  11937  hashgcdlem  11939  ennnfonelemhf1o  11962  ntreq0  12340  ispsmet  12531  psmet0  12535  ismet  12552  isxmet  12553  xmeteq0  12567  metn0  12586  xmetres2  12587  xblss2ps  12612  xblss2  12613  xmseq0  12676  comet  12707  bdxmet  12709  cnmet  12738  ivthdec  12830  reeff1o  12902  ioocosf1o  12983  logbgcd1irr  13092  logbgcd1irraplemexp  13093  pwle2  13366  subctctexmid  13369  peano4nninf  13375  nninfalllemn  13377  nninfalllem1  13378  nninfsellemdc  13381  nninfsellemeq  13385  nninfsellemqall  13386  nninfsellemeqinf  13387  nninfomnilem  13389  nninfomni  13390  isomninnlem  13400  trilpolemlt1  13409  trirec0  13412  iswomninnlem  13417  ismkvnnlem  13419  dceqnconst  13423