Theorem eqeq1d 2198

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182

This theorem is referenced by:  rspcedeq1vd  2865  sbceq2g  3094  csbhypf  3110  csbiebt  3111  csbiebg  3114  dfss4st  3383  disjssun  3501  sneqrg  3777  preq12b  3785  preq12bg  3788  disji2  4011  iin0r  4184  opthg  4253  opeqsn  4267  unisucg  4429  opthreg  4570  tfisi  4601  dmsnopg  5115  relcoi1  5175  iotaeq  5201  iotabi  5202  fneq1  5320  fnun  5338  fnresdisj  5342  fnimadisj  5352  fnimaeq0  5353  sbcfng  5379  foeq1  5450  foco  5464  fveqeq2d  5539  fvelimab  5589  fvun1  5599  fvmptdv2  5622  fneqeql  5641  dffo3  5680  fvsng  5729  fconstfvm  5751  eufnfv  5764  f1veqaeq  5787  dff13f  5788  f1elima  5791  foeqcnvco  5808  f1eqcocnv  5809  acexmidlemab  5886  ovanraleqv  5916  eloprabga  5979  ovmpodv2  6026  ovi3  6029  ovelimab  6043  caovcang  6054  caovcan  6057  caovimo  6086  suppssfv  6098  suppssov1  6099  caofinvl  6124  op1stg  6170  op2ndg  6171  eqop  6197  reldm  6206  xporderlem  6251  tposfo2  6287  frec0g  6417  freccllem  6422  frecfcllem  6424  frecsuclem  6426  frecsuc  6427  nnm0r  6499  nnmord  6537  nnaordex  6548  nnawordex  6549  ereq1  6561  eqerlem  6585  mapsn  6711  endisj  6845  pw2f1odclem  6857  xpf1o  6867  mapxpen  6871  fidifsnen  6893  supelti  7026  updjudhcoinlf  7104  updjudhcoinrg  7105  updjud  7106  omp1eomlem  7118  difinfsnlem  7123  nnnninfeq  7151  enomnilem  7161  finomni  7163  exmidomni  7165  fodjuomnilemres  7171  fodjuomni  7172  ismkvnex  7178  mkvprop  7181  fodjumkvlemres  7182  enmkvlem  7184  enwomnilem  7192  nninfdcinf  7194  nninfwlporlem  7196  nninfwlpoimlemginf  7199  pm54.43  7214  exmidfodomrlemrALT  7227  cc2lem  7290  addnidpig  7360  ltexpi  7361  dfplpq2  7378  dfmpq2  7379  recexnq  7414  recmulnqg  7415  ltexnqq  7432  halfnqq  7434  enq0tr  7458  nqnq0pi  7462  addnnnq0  7473  addlocpr  7560  ltexprlemru  7636  ltexpri  7637  lteupri  7641  prplnqu  7644  recexpr  7662  addsrpr  7769  mulsrpr  7770  00sr  7793  negexsr  7796  recexgt0sr  7797  srpospr  7807  prsrriota  7812  caucvgsrlemfv  7815  map2psrprg  7829  elrealeu  7853  axrnegex  7903  axprecex  7904  rereceu  7913  recriota  7914  nntopi  7918  axcaucvglemval  7921  axcaucvglemcau  7922  cnegexlem1  8157  cnegex  8160  cnegex2  8161  subval  8174  subadd  8185  subadd2  8186  subsub23  8187  addsubeq4  8197  subcan2  8207  negcon1  8234  subcan  8237  addrsub  8353  ltadd2  8401  ltordlem  8464  recexre  8560  recexap  8635  muleqadd  8650  receuap  8651  divvalap  8656  divmulap  8657  rec11ap  8692  rerecapb  8825  zdiv  9366  uzin  9585  xaddval  9870  xnn0xadd0  9892  xnegdi  9893  xltadd1  9901  icc0r  9951  fznlem  10066  fseq1m1p1  10120  1fv  10164  fzon  10191  fvinim0ffz  10266  ioo0  10285  ico0  10287  ioc0  10288  flqbi  10316  divfl0  10322  modq0  10355  modqmuladdnn0  10394  addmodlteq  10424  frecuzrdgtcl  10438  frecuzrdgfunlem  10445  seq3f1olemstep  10527  seq3f1olemp  10528  seq3id  10534  seq3z  10537  qsqeqor  10657  mulreap  10900  rennim  11038  resqrexlemex  11061  rsqrmo  11063  resqrtcl  11065  rersqrtthlem  11066  sqrtsq2  11079  isumss  11426  fsum00  11497  telfsumo  11501  pwm1geoserap1  11543  prodssdc  11624  absefib  11805  efieq1re  11806  divides  11823  dvdsval2  11824  nndivides  11831  dvds0lem  11835  dvds1lem  11836  dvds2lem  11837  negdvdsb  11841  muldvds1  11850  muldvds2  11851  dvdscmulr  11854  dvdsmulcr  11855  dvdstr  11862  dvdsabseq  11880  divconjdvds  11882  odd2np1lem  11904  odd2np1  11905  even2n  11906  oddm1even  11907  2tp1odd  11916  opeo  11929  omeo  11930  m1exp1  11933  divalgb  11957  gcdaddm  12012  gcdabs1  12017  bezout  12039  gcdmultiple  12048  gcdmultiplez  12049  rplpwr  12055  rppwr  12056  alginv  12074  algcvga  12078  algfx  12079  eucalgval2  12080  coprmdvds  12119  qredeq  12123  qredeu  12124  divgcdcoprm0  12128  divgcdcoprmex  12129  cncongr1  12130  rpexp  12180  rpexp12i  12182  cncongrprm  12184  qnumdenbi  12219  phival  12240  phicl2  12241  dfphi2  12247  phiprmpw  12249  phimullem  12252  eulerthlem1  12254  eulerthlemfi  12255  eulerthlemrprm  12256  eulerthlemth  12259  eulerth  12260  fermltl  12261  hashgcdlem  12265  phisum  12267  odzval  12268  odzdvds  12272  reumodprminv  12280  modprm0  12281  nnnn0modprm0  12282  modprmn0modprm0  12283  coprimeprodsq  12284  coprimeprodsq2  12285  pythagtriplem2  12293  pythagtrip  12310  pceulem  12321  pcval  12323  pcqmul  12330  pcqcl  12333  pcabs  12353  pc2dvds  12357  pcaddlem  12366  pcadd  12367  pcmpt  12370  prmpwdvds  12382  pockthi  12385  4sqlem12  12429  ennnfonelemhf1o  12459  fvprif  12812  mgmidmo  12841  grpidvalg  12842  grpidpropdg  12843  ismgmid  12846  ismgmid2  12849  mgmidsssn0  12853  grpinvalem  12854  grprida  12856  ismnddef  12872  sgrpidmndm  12874  ismndd  12891  mndpropd  12894  mndinvmod  12899  mnd1  12900  ismhm  12906  grpinvex  12948  isgrpd2  12959  isgrpd  12961  dfgrp2  12964  grpinveu  12975  grpinvval  12980  grplinv  12987  isgrpinv  12991  grplrinv  12994  grpidinv2  12995  grpidinv  12996  grplmulf1o  13011  grpsubeq0  13023  grpsubadd  13025  dfgrp3mlem  13035  dfgrp3m  13036  grp1  13043  imasgrp2  13045  qusgrp2  13048  mhmmnd  13051  ghmgrp  13053  mulgval  13057  mulgaddcom  13079  eqg0el  13161  ghmeqker  13203  ghmf1  13205  conjnmzb  13212  ablsubadd  13244  ablsubsub23  13257  rngmneg1  13294  rngmneg2  13295  dfur2g  13309  srgideu  13319  srgidmlem  13325  issrgid  13328  srgrz  13331  srglz  13332  srgisid  13333  srg1zr  13334  ringideu  13364  ringidmlem  13369  isringid  13372  ringid  13373  qusring2  13409  oppr0g  13424  oppr1g  13425  reldvdsrsrg  13435  dvdsrvald  13436  dvdsrmuld  13439  dvdsr01  13447  dvdsr02  13448  opprunitd  13453  crngunit  13454  unitinvinv  13467  dvreq1  13485  dvdsrpropdg  13490  rhmdvdsr  13518  lringuplu  13536  subrg1  13571  subrgdvds  13575  islmod  13600  islmodd  13602  lmodprop2d  13657  lss1d  13692  znval  13925  ntreq0  14069  ispsmet  14260  psmet0  14264  ismet  14281  isxmet  14282  xmeteq0  14296  metn0  14315  xmetres2  14316  xblss2ps  14341  xblss2  14342  xmseq0  14405  comet  14436  bdxmet  14438  cnmet  14467  ivthdec  14559  reeff1o  14631  ioocosf1o  14712  logbgcd1irr  14822  logbgcd1irraplemexp  14823  lgsval  14842  lgsdir  14873  lgsne0  14876  lgsprme0  14880  lgsdirnn0  14885  lgseisenlem2  14888  m1lgs  14889  2sqlem7  14905  2sqlem8  14907  2sqlem9  14908  bj-charfunbi  15000  pwle2  15186  subctctexmid  15188  peano4nninf  15193  nninfalllem1  15195  nninfsellemdc  15197  nninfsellemeq  15201  nninfsellemqall  15202  nninfsellemeqinf  15203  isomninnlem  15216  trilpolemlt1  15227  trirec0  15230  iswomninnlem  15235  iswomni0  15237  ismkvnnlem  15238  dceqnconst  15246  dcapnconst  15247