Theorem eqeq1d 2148

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  rspcedeq1vd  2798  sbceq2g  3024  csbhypf  3038  csbiebt  3039  csbiebg  3042  dfss4st  3309  disjssun  3426  sneqrg  3689  preq12b  3697  preq12bg  3700  disji2  3922  iin0r  4093  opthg  4160  opeqsn  4174  unisucg  4336  opthreg  4471  tfisi  4501  dmsnopg  5010  relcoi1  5070  iotaeq  5096  iotabi  5097  fneq1  5211  fnun  5229  fnresdisj  5233  fnimadisj  5243  fnimaeq0  5244  sbcfng  5270  foeq1  5341  foco  5355  fveqeq2d  5429  fvelimab  5477  fvun1  5487  fvmptdv2  5510  fneqeql  5528  dffo3  5567  fvsng  5616  fconstfvm  5638  eufnfv  5648  f1veqaeq  5670  dff13f  5671  f1elima  5674  foeqcnvco  5691  f1eqcocnv  5692  acexmidlemab  5768  ovanraleqv  5798  eloprabga  5858  ovmpodv2  5904  ovi3  5907  ovelimab  5921  caovcang  5932  caovcan  5935  caovimo  5964  grprinvlem  5965  grpridd  5967  suppssfv  5978  suppssov1  5979  caofinvl  6004  op1stg  6048  op2ndg  6049  eqop  6075  reldm  6084  xporderlem  6128  tposfo2  6164  frec0g  6294  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnm0r  6375  nnmord  6413  nnaordex  6423  nnawordex  6424  ereq1  6436  eqerlem  6460  mapsn  6584  endisj  6718  xpf1o  6738  mapxpen  6742  fidifsnen  6764  supelti  6889  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  omp1eomlem  6979  difinfsnlem  6984  enomnilem  7010  finomni  7012  exmidomni  7014  fodjuomnilemres  7020  fodjuomni  7021  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  pm54.43  7046  exmidfodomrlemrALT  7059  addnidpig  7144  ltexpi  7145  dfplpq2  7162  dfmpq2  7163  recexnq  7198  recmulnqg  7199  ltexnqq  7216  halfnqq  7218  enq0tr  7242  nqnq0pi  7246  addnnnq0  7257  addlocpr  7344  ltexprlemru  7420  ltexpri  7421  lteupri  7425  prplnqu  7428  recexpr  7446  addsrpr  7553  mulsrpr  7554  00sr  7577  negexsr  7580  recexgt0sr  7581  srpospr  7591  prsrriota  7596  caucvgsrlemfv  7599  map2psrprg  7613  elrealeu  7637  axrnegex  7687  axprecex  7688  rereceu  7697  recriota  7698  nntopi  7702  axcaucvglemval  7705  axcaucvglemcau  7706  cnegexlem1  7937  cnegex  7940  cnegex2  7941  subval  7954  subadd  7965  subadd2  7966  subsub23  7967  addsubeq4  7977  subcan2  7987  negcon1  8014  subcan  8017  addrsub  8133  ltadd2  8181  ltordlem  8244  recexre  8340  recexap  8414  muleqadd  8429  receuap  8430  divvalap  8434  divmulap  8435  rec11ap  8470  zdiv  9139  uzin  9358  xaddval  9628  xnn0xadd0  9650  xnegdi  9651  xltadd1  9659  icc0r  9709  fznlem  9821  fseq1m1p1  9875  1fv  9916  fzon  9943  fvinim0ffz  10018  ioo0  10037  ico0  10039  ioc0  10040  flqbi  10063  divfl0  10069  modq0  10102  modqmuladdnn0  10141  addmodlteq  10171  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  seq3f1olemstep  10274  seq3f1olemp  10275  seq3id  10281  seq3z  10284  mulreap  10636  rennim  10774  resqrexlemex  10797  rsqrmo  10799  resqrtcl  10801  rersqrtthlem  10802  sqrtsq2  10815  isumss  11160  fsum00  11231  telfsumo  11235  pwm1geoserap1  11277  absefib  11477  efieq1re  11478  divides  11495  dvdsval2  11496  nndivides  11500  dvds0lem  11503  dvds1lem  11504  dvds2lem  11505  negdvdsb  11509  muldvds1  11518  muldvds2  11519  dvdscmulr  11522  dvdsmulcr  11523  dvdstr  11530  dvdsabseq  11545  divconjdvds  11547  odd2np1lem  11569  odd2np1  11570  even2n  11571  oddm1even  11572  2tp1odd  11581  opeo  11594  omeo  11595  m1exp1  11598  divalgb  11622  gcdaddm  11672  gcdabs1  11677  bezout  11699  gcdmultiple  11708  gcdmultiplez  11709  rplpwr  11715  rppwr  11716  alginv  11728  algcvga  11732  algfx  11733  eucalgval2  11734  coprmdvds  11773  qredeq  11777  qredeu  11778  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  rpexp  11831  rpexp12i  11833  cncongrprm  11835  qnumdenbi  11870  phival  11889  phicl2  11890  dfphi2  11896  phiprmpw  11898  phimullem  11901  hashgcdlem  11903  ennnfonelemhf1o  11926  ntreq0  12301  ispsmet  12492  psmet0  12496  ismet  12513  isxmet  12514  xmeteq0  12528  metn0  12547  xmetres2  12548  xblss2ps  12573  xblss2  12574  xmseq0  12637  comet  12668  bdxmet  12670  cnmet  12699  ivthdec  12791  pwle2  13193  subctctexmid  13196  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfsellemdc  13206  nninfsellemeq  13210  nninfsellemqall  13211  nninfsellemeqinf  13212  nninfomnilem  13214  nninfomni  13215  isomninnlem  13225  trilpolemlt1  13234